naproch sty extension

1 files changed, 19 insertions, 14 deletions

diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex
index c3c72f0..b8a5fa5 100644
--- a/library/topology/urysohn.tex
+++ b/library/topology/urysohn.tex
@@ -504,26 +504,31 @@ The first tept will be a formalisation of chain constructions.
 
 
  
-\begin{definition}\label{sequencetwo}
-   $Z$ is a sequencetwo iff  $Z = (N,f,B)$ and $N \subseteq \naturals$ and $f$ is a bijection from $N$ to $B$.
-\end{definition}
-
-\begin{proposition}\label{sequence_existence}
-    Suppose $N \subseteq \naturals$.
-    Suppose $M \subseteq \naturals$.
-    Suppose $N = M$.
-    Then there exist $Z,f$ such that $f$ is a bijection from $N$ to $M$ and $Z=(N,f,M)$ and $Z$ is a sequencetwo.
-\end{proposition}
-\begin{proof}
-    Let $f(x) = x$ for $x \in N$.
-    Let $Z=(N,f,M)$.
-\end{proof}
+%\begin{definition}\label{sequencetwo}
+%   $Z$ is a sequencetwo iff  $Z = (N,f,B)$ and $N \subseteq \naturals$ and $f$ is a bijection from $N$ to $B$.
+%\end{definition}
+%
+%\begin{proposition}\label{sequence_existence}
+%    Suppose $N \subseteq \naturals$.
+%    Suppose $M \subseteq \naturals$.
+%    Suppose $N = M$.
+%    Then there exist $Z,f$ such that $f$ is a bijection from $N$ to $M$ and $Z=(N,f,M)$ and $Z$ is a sequencetwo.
+%\end{proposition}
+%\begin{proof}
+%    Let $f(x) = x$ for $x \in N$.
+%    Let $Z=(N,f,M)$.
+%\end{proof}
 %The proposition above and the definition prove false together with
 % ordinal_subseteq_unions, omega_is_an_ordinal, powerset_intro, in_irrefl
 
 
 
 
+
+
+
+
+
 \begin{theorem}\label{urysohn}
     Let $X$ be a urysohn space.
     Suppose $A,B \in \closeds{X}$.