1 files changed, 66 insertions, 0 deletions
diff --git a/test/phase5/exact-structure.tex b/test/phase5/exact-structure.tex
index b1a0d86..fb34abe 100644
--- a/test/phase5/exact-structure.tex
+++ b/test/phase5/exact-structure.tex
@@ -25,3 +25,69 @@
 \begin{proof}
     Follows by assumption.
 \end{proof}
+
+\begin{proposition}\label{pointed_self_member}
+    Let $X$ be a pointed set.
+    Then $X \in X$.
+\end{proposition}
+\begin{proof}
+    Follows.
+\end{proof}
+
+\begin{proposition}\label{pointed_self_member_explicit}
+    Let $X$ be a pointed set.
+    Then $X \in \carrier[X]$.
+\end{proposition}
+\begin{proof}
+    Follows.
+\end{proof}
+
+\begin{proposition}\label{pointed_self_not_member}
+    Let $X$ be a pointed set.
+    Then $X \notin X$.
+\end{proposition}
+\begin{proof}
+    Follows.
+\end{proof}
+
+\begin{proposition}\label{pointed_self_not_member_explicit}
+    Let $X$ be a pointed set.
+    Then $X \notin \carrier[X]$.
+\end{proposition}
+\begin{proof}
+    Follows.
+\end{proof}
+
+\begin{proposition}\label{pointed_self_element}
+    Let $X$ be a pointed set.
+    Then $X$ is an element of $X$.
+\end{proposition}
+\begin{proof}
+    Follows.
+\end{proof}
+
+\begin{proposition}\label{pointed_self_element_explicit}
+    Let $X$ be a pointed set.
+    Then $X$ is an element of $\carrier[X]$.
+\end{proposition}
+\begin{proof}
+    Follows.
+\end{proof}
+
+\begin{proposition}\label{pointed_header_member}
+    Let $X$ be a pointed set.
+    Let $x \in X$.
+    Then $x = x$.
+\end{proposition}
+\begin{proof}
+    Follows.
+\end{proof}
+
+\begin{proposition}\label{pointed_header_member_explicit}
+    Let $X$ be a pointed set.
+    Let $x \in \carrier[X]$.
+    Then $x = x$.
+\end{proposition}
+\begin{proof}
+    Follows.
+\end{proof}