1 files changed, 16 insertions, 0 deletions
diff --git a/test/phase5/exact-relational-replacement.tex b/test/phase5/exact-relational-replacement.tex
new file mode 100644
index 0000000..43ef06f
--- /dev/null
+++ b/test/phase5/exact-relational-replacement.tex
@@ -0,0 +1,16 @@
+\begin{axiom}\label{phase5_relational_support}
+    For every set $A$ we have $A = A$.
+\end{axiom}
+
+\begin{definition}\label{phase5_relational_replacement_definition}
+    $\phasefiverelational{A} = \{ y \mid \exists x\in A. y = x \}$.
+\end{definition}
+
+\begin{proposition}\label{phase5_relational_replacement_local}
+    For every set $A$ we have $A = A$.
+\end{proposition}
+\begin{proof}
+    Fix $A$.
+    Let $B = \{ y \mid \exists x\in A. y = x \}$.
+    Follows.
+\end{proof}