Corrected Contradiction.

Contradiction was due to a misstake in the definition in sequence.

1 files changed, 4 insertions, 1 deletions

diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex
index 7f98bc2..f70d679 100644
--- a/library/topology/urysohn2.tex
+++ b/library/topology/urysohn2.tex
@@ -41,7 +41,7 @@
 
 
 \begin{definition}\label{sequence}
-    $X$ is a sequence iff $X$ is a function and $\dom{f} \subseteq \naturals$.
+    $X$ is a sequence iff $X$ is a function and $\dom{X} \subseteq \naturals$.
 \end{definition}
 
 
@@ -169,6 +169,9 @@
 \begin{theorem}\label{safe}
     Contradiction.     
 \end{theorem}
+\begin{proof}
+    Follows by \cref{iff_sequence,codom_of_emptyset_can_be_anything,sequence,emptyset_is_function_on_emptyset,id_dom,in_irrefl,suc_subseteq_implies_in,emptyset_subseteq}. 
+\end{proof}