From 65e5a741655d8339ad5763e365ea2addd2e96e51 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Fri, 9 Aug 2024 15:15:49 +0200
Subject: put cardinalit to the right place

---
 library/cardinal.tex | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'library/cardinal.tex')

diff --git a/library/cardinal.tex b/library/cardinal.tex
index d0dec59..8691b30 100644
--- a/library/cardinal.tex
+++ b/library/cardinal.tex
@@ -3,6 +3,7 @@
 \import{set.tex}
 \import{ordinal.tex}
 \import{function.tex}
+\import{numbers.tex}
 
 \begin{definition}\label{finite}
     $X$ is finite iff there exists a natural number $k$ such that
@@ -12,3 +13,8 @@
 \begin{abbreviation}\label{infinite}
     $X$ is infinite iff $X$ is not finite.
 \end{abbreviation}
+
+\begin{definition}\label{cardinality}
+    $X$ has cardinality $k$ iff $k$ is a natural number and 
+    there exists a bijection from $k$ to $X$.
+\end{definition}
-- 
cgit v1.2.3


From 34aad4be8fb8433f0205517732da0d449d077572 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Sat, 10 Aug 2024 19:18:39 +0200
Subject: more more urysohn

---
 library/cardinal.tex         |   2 +
 library/topology/urysohn.tex | 341 ++++++++++++++++++++++++-------------------
 2 files changed, 190 insertions(+), 153 deletions(-)

(limited to 'library/cardinal.tex')

diff --git a/library/cardinal.tex b/library/cardinal.tex
index 8691b30..044e5d1 100644
--- a/library/cardinal.tex
+++ b/library/cardinal.tex
@@ -18,3 +18,5 @@
     $X$ has cardinality $k$ iff $k$ is a natural number and 
     there exists a bijection from $k$ to $X$.
 \end{definition}
+
+
diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex
index 3152de7..028e10f 100644
--- a/library/topology/urysohn.tex
+++ b/library/topology/urysohn.tex
@@ -198,60 +198,82 @@ The first tept will be a formalisation of chain constructions.
     Let $X$ be a urysohn space.
     Suppose $A,B \in \closeds{X}$.
     Suppose $A \inter B$ is empty.
-    Suppose $U = \{A,(X \setminus B)\}$.
-    Suppose $\indexset[U]= \{\zero, 1\}$.
-    Suppose $\index[U](\zero) = A$.
-    Suppose $\index[U](1) = (X \setminus B)$.
-    Then $U$ is a urysohnchain in $X$.
+    Then there exist $U$
+    such that $\carrier[U] = \{A,(\carrier[X] \setminus B)\}$
+    and $\indexset[U]= \{\zero, 1\}$
+    and $\index[U](\zero) = A$
+    and $\index[U](1) = (\carrier[X] \setminus B)$.
+    %$U$ is a urysohnchain in $X$.
 \end{proposition}
 \begin{proof}
-    We show that $U$ is a sequence.
-    \begin{subproof}
-        Omitted.
-    \end{subproof}
 
-    We show that $A \subseteq (X \setminus B)$.
-    \begin{subproof}
-        Omitted.
-    \end{subproof}
+    Omitted.
 
-    We show that $U$ is a chain of subsets.
-    \begin{subproof}
-        For all $n \in \indexset[U]$ we have $n = \zero \lor n = 1$.
-        It suffices to show that for all $n \in \indexset[U]$ we have
-        for all $m \in \indexset[U]$ such that 
-        $n < m$ we have $\index[U](n) \subseteq \index[U](m)$.
-        Fix $n \in \indexset[U]$.
-        Fix $m \in \indexset[U]$.
-        \begin{byCase}
-            \caseOf{$n = 1$.} Trivial.
-            \caseOf{$n = \zero$.} 
-                \begin{byCase}
-                    \caseOf{$m = \zero$.} Trivial.
-                    \caseOf{$m = 1$.} Omitted.
-                \end{byCase}
-        \end{byCase}
-    \end{subproof}
+    %   We show that $U$ is a sequence.
+    %   \begin{subproof}
+    %       Omitted.
+    %   \end{subproof}
+%   
+    %   We show that $A \subseteq (\carrier[X] \setminus B)$.
+    %   \begin{subproof}
+    %       Omitted.
+    %   \end{subproof}
+%   
+    %   We show that $U$ is a chain of subsets.
+    %   \begin{subproof}
+    %       For all $n \in \indexset[U]$ we have $n = \zero \lor n = 1$.
+    %       It suffices to show that for all $n \in \indexset[U]$ we have
+    %       for all $m \in \indexset[U]$ such that 
+    %       $n < m$ we have $\index[U](n) \subseteq \index[U](m)$.
+    %       Fix $n \in \indexset[U]$.
+    %       Fix $m \in \indexset[U]$.
+    %       \begin{byCase}
+    %           \caseOf{$n = 1$.} Trivial.
+    %           \caseOf{$n = \zero$.} 
+    %               \begin{byCase}
+    %                   \caseOf{$m = \zero$.} Trivial.
+    %                   \caseOf{$m = 1$.} Omitted.
+    %               \end{byCase}
+    %       \end{byCase}
+    %   \end{subproof}
+%   
+    %   $A \subseteq X$.
+    %   $(X \setminus B) \subseteq X$.
+    %   We show that for all $x \in U$ we have $x \subseteq X$.
+    %   \begin{subproof}
+    %       Omitted.
+    %   \end{subproof}
+%   
+    %   We show that $\closure{A}{X} \subseteq \interior{(X \setminus B)}{X}$.
+    %   \begin{subproof}
+    %       Omitted.
+    %   \end{subproof}
+    %   We show that for all $n,m \in \indexset[U]$ such that $n < m$ we have
+    %   $\closure{\index[U](n)}{X} \subseteq \interior{\index[U](m)}{X}$.
+    %   \begin{subproof}
+    %       Omitted.
+    %   \end{subproof}
 
-    $A \subseteq X$.
-    $(X \setminus B) \subseteq X$.
-    We show that for all $x \in U$ we have $x \subseteq X$.
-    \begin{subproof}
-        Omitted.
-    \end{subproof}
+    
+\end{proof}
 
-    We show that $\closure{A}{X} \subseteq \interior{(X \setminus B)}{X}$.
-    \begin{subproof}
-        Omitted.
-    \end{subproof}
-    We show that for all $n,m \in \indexset[U]$ such that $n < m$ we have
-    $\closure{\index[U](n)}{X} \subseteq \interior{\index[U](m)}{X}$.
-    \begin{subproof}
-        Omitted.
-    \end{subproof}
+\begin{proposition}\label{urysohnchain_induction_begin_step_two}
+    Let $X$ be a urysohn space.
+    Suppose $A,B \in \closeds{X}$.
+    Suppose $A \inter B$ is empty.
+    Suppose there exist $U$
+    such that $\carrier[U] = \{A,(\carrier[X] \setminus B)\}$
+    and $\indexset[U]= \{\zero, 1\}$
+    and $\index[U](\zero) = A$
+    and $\index[U](1) = (\carrier[X] \setminus B)$.
+    Then $U$ is a urysohnchain in $X$.
+\end{proposition}
+\begin{proof}
+    Omitted.
 \end{proof}
 
 
+
 \begin{proposition}\label{t_four_propositon}
     Let $X$ be a urysohn space.
     Then for all $A,B \subseteq X$ such that $\closure{A}{X} \subseteq \interior{B}{X}$
@@ -295,134 +317,147 @@ The first tept will be a formalisation of chain constructions.
 \end{proof}
 
 
+\begin{proposition}\label{existence_of_staircase_function}
+    Let $X$ be a urysohn space.
+    Suppose $U$ is a urysohnchain in $X$ and $U$ has cardinality $k$.
+    Suppose $k \neq \zero$.
+    Then there exist $f$ such that $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ 
+    and for all $n \in \indexset[U]$ we have for all $x \in \index[U](n)$ 
+    we have $f(x) = \rfrac{n}{k}$.
+\end{proposition}
+\begin{proof}
+    Omitted.
+\end{proof}
 
+\begin{abbreviation}\label{refinment_abbreviation}
+    $x \refine y$ iff $x$ is a refinmant of $y$.
+\end{abbreviation}
 
 
 
 
-
-
-%                    The next thing we need to define is the uniform staircase function.
-%                    This function has it's domain in $X$ and maps to the closed interval $[0,1]$.
-%                    These functions should behave als follows,
-%                    \begin{align}
-%                        &f(A_{0}) = 1 &\text{consant} \\
-%                        &f(A_{k} \setminus A_{k+1}) = 1-\frac{k}{r} &\text{constant.}
-%                    \end{align} 
-
-%                    We then prove that for any given $r$ we find a repolished chain,
-%                    which contains the $A_{i}$ and this replished chain is also legal.
-%                     
-%                    The proof will be finished by taking the limit on $f_{n}$ with $f_{n}$ 
-%                    be a staircase function with $n$ many refinemants. 
-%                    This limit will be continuous and we would be done. 
-
-
-% TODO: Since we want to prove that $f$ is continus, we have to formalize that 
-% \reals with the usual topology is a topological space. 
-% -------------------------------------------------------------
-
 \begin{theorem}\label{urysohn}
     Let $X$ be a urysohn space.
     Suppose $A,B \in \closeds{X}$.
     Suppose $A \inter B$ is empty.
-    There exist $f$ such that $f \in \funs{X}{\intervalclosed{\zero}{1}}$ 
+    There exist $f$ such that $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ 
     and $f(A) = 1$ and $f(B)= 0$ and $f$ is continuous.
 \end{theorem}
 \begin{proof}
-    We show that for all $n \in \naturals$ we have
-    if there exist $C$ such that $C$ is a urysohnchain in $X$ of cardinality $n$ 
-    then there exist $C'$  such that $C'$ is a urysohnchain in $X$ of cardinality $n+1$ 
-    and $C'$ is a refinmant of $C$.
-    \begin{subproof}
-        Omitted.
-    \end{subproof}
-
-    There exist $\eta$ such that $\eta$ is a urysohnchain in $X$ and $\eta =\{A, (x \setminus B)\}$.
-
-    
 
-    Take $P$ such that $P$ is a infinite sequence and $\indexset[P] = \naturals$ and for all $i \in \indexset[P]$ we have $\index[P](i) = \pow{X}$.
+    There exist $\eta$ such that $\carrier[\eta] = \{A, (\carrier[X] \setminus B)\}$ 
+    and $\indexset[\eta] = \{\zero, 1\}$ 
+    and $\index[\eta](\zero) = A$
+    and $\index[\eta](1) = (\carrier[X] \setminus B)$  by \cref{urysohnchain_induction_begin}.
     
-    We show that there exist $\zeta$ such that $\zeta$ is a infinite sequence 
-    and for all $i \in \indexset[\zeta]$ we have 
-    $\index[\zeta](i)$ is a urysohnchain in $X$ of cardinality $i$
-    and $A \subseteq \index[\zeta](i)$
-    and $\index[\zeta](i) \subseteq (X \setminus B)$
-    and for all $j \in \indexset[\zeta]$ such that 
-    $j < i$ we have for all $x \in \index[\zeta](j)$ we have $x \in \index[\zeta](i)$.
+    We show that there exist $\zeta$ such that $\zeta$ is a sequence 
+    and $\indexset[\zeta] = \naturals$
+    and $\eta \in \carrier[\zeta]$ and $\index[\zeta](\eta) = \zero$
+    and for all $n \in \indexset[\zeta]$ we have $n+1 \in \indexset[\zeta]$ 
+    and $\index[\zeta](n+1)$ is a refinmant of $\index[\zeta](n)$.
     \begin{subproof}
-        Omitted.
-    \end{subproof}
-  
-    
-
-
-    
-
+        %Let $P = \{ n \in \naturals \mid \exists \zeta. ((n = \zero \land \index[\zeta](n) = \eta \land \index[\zeta](n+1)$ is a refinmant of $\index[\zeta](n)) \lor (n \neq \zero \land \index[\zeta](n)$ is a urysohnchain in $X$ \land $\index[\zeta](n+1)$ is a refinmant of $\index[\zeta](n)))\}$.
+        %Let $C = \{ x \mid \text{$x$ is a uysohncahin in $X$}\}$.
+        Let $\alpha = \{x \in C \mid \exists y \in \alpha. x \refine y \lor x = \eta\}$.
+        Let $\beta = \{ (n,x) \mid n \in \naturals \mid \exists m \in \naturals. \exists y \in \alpha. (x \in \alpha) \land ((x \refine y \land m = n+1 )\lor ((n,x) = (\zero,\eta)))\}$.
 
-
-    We show that there exist $g \in \funs{X}{\intervalclosed{\zero}{1}}$ such that $g(A)=1$ and $g(X\setminus A) = \zero$.
-    \begin{subproof}
-        Omitted.
+        % TODO: Proof that \beta is a function which would be used for the indexing.
+        
     \end{subproof}
-    $g$ is a staircase function and $\chain[g] = C$.
-    $g$ is a legal staircase function.
 
 
-    We show that there exist $f$ such that $f \in \funs{X}{\intervalclosed{\zero}{1}}$ 
-    and $f(A) = 1$ and $f(B)= 0$ and $f$ is continuous.
-    \begin{subproof}
-        Omitted.
-    \end{subproof}
 
 
-    %We show that for all $n \in \nautrals$ we have $C_{n}$ a legal chain of subsets of $X$. 
-    %\begin{subproof}
-    %    Omitted.
-    %\end{subproof}
-
-    %Proof Sheme Idea:
-    % -We proof for n=1 that C_{n} is a chain and legal
-    % -Then by induction with P(n+1) is refinmant of P(n)
-    % -Therefore we have a increing refinmant of these Chains such that our limit could even apply
-    % ---------------------------------------------------------
-
-    %We show that there exist $f \in \funs{\naturals}{\funs{X}{\intervalclosed{0}{1}}}$ such that $f(n)$ is a staircase function. %TODO: Define Staircase function
-    %\begin{subproof}
-    %    Omitted.
-    %\end{subproof}
-
-
-    % Formalization idea of enumarted sequences:
-    % - Define a enumarted sequnecs as a set A with a bijection between A and E \in \pow{\naturals} 
-    % - This should give all finite and infinte enumarable sequences
-    % - Introduce a notion for the indexing of these enumarable sequences.
-    % - Then we can define the limit of a enumarted sequence of functions.
-    % ---------------------------------------------------------
-    %
-    % Here we need a limit definition for sequences of functions
-    %We show that there exist $F \in \funs{X}{\intervalclosed{0}{1}}$ such that $F = \limit{set of the staircase functions}$
-    %\begin{subproof}
-    %    Omitted.
-    %\end{subproof}
-    %
-    %We show that $F(A) = 1$.
-    %\begin{subproof}
-    %    Omitted.
-    %\end{subproof}
-    %
-    %We show that $F(B) = 0$.
-    %\begin{subproof}
-    %    Omitted.
-    %\end{subproof} 
-    %
-    %We show that $F$ is continuous.
-    %\begin{subproof}
-    %    Omitted.
-    %\end{subproof}
+    %Suppose $\eta$ is a urysohnchain in $X$.
+    %Suppose $\carrier[\eta] =\{A, (X \setminus B)\}$
+    %and $\indexset[\eta] = \{\zero, 1\}$
+    %and $\index[\eta](\zero) = A$ 
+    %and $\index[\eta](1) = (X \setminus B)$.
+
+
+    %Then $\eta$ is a urysohnchain in $X$.
+
+    %   Take $P$ such that $P$ is a infinite sequence and $\indexset[P] = \naturals$ and for all $i \in \indexset[P]$ we have $\index[P](i) = \pow{X}$.
+    %   
+    %   We show that there exist $\zeta$ such that $\zeta$ is a infinite sequence 
+    %   and for all $i \in \indexset[\zeta]$ we have 
+    %   $\index[\zeta](i)$ is a urysohnchain in $X$ of cardinality $i$
+    %   and $A \subseteq \index[\zeta](i)$
+    %   and $\index[\zeta](i) \subseteq (X \setminus B)$
+    %   and for all $j \in \indexset[\zeta]$ such that 
+    %   $j < i$ we have for all $x \in \index[\zeta](j)$ we have $x \in \index[\zeta](i)$.
+    %   \begin{subproof}
+    %       Omitted.
+    %   \end{subproof}
+    %   
+    %   
+    %   
+    %   
+    %   
+    %   
+    %   
+    %   
+    %   We show that there exist $g \in \funs{X}{\intervalclosed{\zero}{1}}$ such that $g(A)=1$ and $g(X\setminus A) = \zero$.
+    %   \begin{subproof}
+    %       Omitted.
+    %   \end{subproof}
+    %   $g$ is a staircase function and $\chain[g] = C$.
+    %   $g$ is a legal staircase function.
+    %   
+    %   
+    %   We show that there exist $f$ such that $f \in \funs{X}{\intervalclosed{\zero}{1}}$ 
+    %   and $f(A) = 1$ and $f(B)= 0$ and $f$ is continuous.
+    %   \begin{subproof}
+    %       Omitted.
+    %   \end{subproof}
+
+
+    %   We show that for all $n \in \nautrals$ we have $C_{n}$ a legal chain of subsets of $X$. 
+    %   \begin{subproof}
+    %       Omitted.
+    %   \end{subproof}
+
+    %   Proof Sheme Idea:
+    %    -We proof for n=1 that C_{n} is a chain and legal
+    %    -Then by induction with P(n+1) is refinmant of P(n)
+    %    -Therefore we have a increing refinmant of these Chains such that our limit could even apply
+    %    ---------------------------------------------------------
+
+    %   We show that there exist $f \in \funs{\naturals}{\funs{X}{\intervalclosed{0}{1}}}$ such that $f(n)$ is a staircase function. %TODO: Define Staircase function
+    %   \begin{subproof}
+    %       Omitted.
+    %   \end{subproof}
+
+
+    %    Formalization idea of enumarted sequences:
+    %    - Define a enumarted sequnecs as a set A with a bijection between A and E \in \pow{\naturals} 
+    %    - This should give all finite and infinte enumarable sequences
+    %    - Introduce a notion for the indexing of these enumarable sequences.
+    %    - Then we can define the limit of a enumarted sequence of functions.
+    %    ---------------------------------------------------------
+    %   
+    %    Here we need a limit definition for sequences of functions
+    %   We show that there exist $F \in \funs{X}{\intervalclosed{0}{1}}$ such that $F = \limit{set of the staircase functions}$
+    %   \begin{subproof}
+    %       Omitted.
+    %   \end{subproof}
+    %   
+    %   We show that $F(A) = 1$.
+    %   \begin{subproof}
+    %       Omitted.
+    %   \end{subproof}
+    %   
+    %   We show that $F(B) = 0$.
+    %   \begin{subproof}
+    %       Omitted.
+    %   \end{subproof} 
+    %   
+    %   We show that $F$ is continuous.
+    %   \begin{subproof}
+    %       Omitted.
+    %   \end{subproof}
 \end{proof}
 
-\begin{theorem}\label{safe}
-    Contradiction.     
-\end{theorem}
+%\begin{theorem}\label{safe}
+%    Contradiction.     
+%\end{theorem}
-- 
cgit v1.2.3


From f6b22fd533bd61e9dbcb6374295df321de99b1f2 Mon Sep 17 00:00:00 2001
From: Simon-Kor <52245124+Simon-Kor@users.noreply.github.com>
Date: Mon, 23 Sep 2024 03:05:41 +0200
Subject: Abgabe

---
 library/algebra/group.tex                   |  2 +-
 library/algebra/monoid.tex                  |  2 +-
 library/cardinal.tex                        |  2 +-
 library/numbers.tex                         |  2 +-
 library/topology/basis.tex                  |  2 +-
 library/topology/continuous.tex             |  2 ++
 library/topology/metric-space.tex           |  4 ++--
 library/topology/real-topological-space.tex |  2 +-
 library/topology/separation.tex             |  2 ++
 library/topology/topological-space.tex      |  2 +-
 library/topology/urysohn.tex                |  4 ++--
 library/topology/urysohn2.tex               | 18 ++++++++++++++----
 12 files changed, 29 insertions(+), 15 deletions(-)

(limited to 'library/cardinal.tex')

diff --git a/library/algebra/group.tex b/library/algebra/group.tex
index 7de1051..449bacb 100644
--- a/library/algebra/group.tex
+++ b/library/algebra/group.tex
@@ -1,5 +1,5 @@
 \import{algebra/monoid.tex}
-\section{Group}
+\section{Group}\label{form_sec_group}
 
 \begin{struct}\label{group}
     A group $G$ is a monoid such that
diff --git a/library/algebra/monoid.tex b/library/algebra/monoid.tex
index 06fcb50..3249a93 100644
--- a/library/algebra/monoid.tex
+++ b/library/algebra/monoid.tex
@@ -1,5 +1,5 @@
 \import{algebra/semigroup.tex}
-\section{Monoid}
+\section{Monoid}\label{form_sec_monoid}
 
 \begin{struct}\label{monoid}
     A monoid $A$ is a semigroup equipped with
diff --git a/library/cardinal.tex b/library/cardinal.tex
index 044e5d1..5682619 100644
--- a/library/cardinal.tex
+++ b/library/cardinal.tex
@@ -1,4 +1,4 @@
-\section{Cardinality}
+\section{Cardinality}\label{form_sec_cardinality}
 
 \import{set.tex}
 \import{ordinal.tex}
diff --git a/library/numbers.tex b/library/numbers.tex
index ac0a683..d3af3f1 100644
--- a/library/numbers.tex
+++ b/library/numbers.tex
@@ -4,7 +4,7 @@
 \import{ordinal.tex}
 
 
-\section{The real numbers}
+\section{The numbers}\label{form_sec_numbers}
 
 \begin{signature}
     $\reals$ is a set.
diff --git a/library/topology/basis.tex b/library/topology/basis.tex
index 052c551..f0f77e4 100644
--- a/library/topology/basis.tex
+++ b/library/topology/basis.tex
@@ -2,7 +2,7 @@
 \import{set.tex}
 \import{set/powerset.tex}
 
-\subsection{Topological basis}
+\subsection{Topological basis}\label{form_sec_topobasis}
 
 \begin{abbreviation}\label{covers}
     $C$ covers $X$ iff
diff --git a/library/topology/continuous.tex b/library/topology/continuous.tex
index a9bc58e..95c4d0a 100644
--- a/library/topology/continuous.tex
+++ b/library/topology/continuous.tex
@@ -3,6 +3,8 @@
 \import{function.tex}
 \import{set.tex}
 
+\subsection{Continuous}\label{form_sec_continuous}
+
 \begin{definition}\label{continuous}
     $f$ is continuous iff for all $U \in \opens[Y]$ we have $\preimg{f}{U} \in \opens[X]$.
 \end{definition}
diff --git a/library/topology/metric-space.tex b/library/topology/metric-space.tex
index 0ed7bab..031aa0f 100644
--- a/library/topology/metric-space.tex
+++ b/library/topology/metric-space.tex
@@ -4,10 +4,10 @@
 \import{set/powerset.tex}
 \import{topology/basis.tex}
 
-\section{Metric Spaces}
+\section{Metric Spaces}\label{form_sec_metric}
 
 \begin{definition}\label{metric}
-    $f$ is a metric on $M$ iff $f$ is a function from $M \times M$ to $\reaaals$ and
+    $f$ is a metric on $M$ iff $f$ is a function from $M \times M$ to $\reals$ and
     for all $x,y,z \in M$ we have 
         $f(x,x) = \zero$ and 
         $f(x,y) = f(y,x)$ and
diff --git a/library/topology/real-topological-space.tex b/library/topology/real-topological-space.tex
index c76fd46..db7ee94 100644
--- a/library/topology/real-topological-space.tex
+++ b/library/topology/real-topological-space.tex
@@ -11,7 +11,7 @@
 \import{function.tex}
 
 
-\section{Topology Reals}
+\section{Topology Reals}\label{form_sec_toporeals}
 
 \begin{definition}\label{topological_basis_reals_eps_ball}
     $\topoBasisReals = \{ \epsBall{x}{\epsilon} \mid x \in \reals, \epsilon \in \realsplus\}$.
diff --git a/library/topology/separation.tex b/library/topology/separation.tex
index 0c68290..aaa3907 100644
--- a/library/topology/separation.tex
+++ b/library/topology/separation.tex
@@ -1,6 +1,8 @@
 \import{topology/topological-space.tex}
 \import{set.tex}
 
+\subsection{Separation}\label{form_sec_separation}
+
 % T0 separation
 \begin{definition}\label{is_kolmogorov}
     $X$ is Kolmogorov iff
diff --git a/library/topology/topological-space.tex b/library/topology/topological-space.tex
index f8bcb93..409e107 100644
--- a/library/topology/topological-space.tex
+++ b/library/topology/topological-space.tex
@@ -2,7 +2,7 @@
 \import{set/powerset.tex}
 \import{set/cons.tex}
 
-\section{Topological spaces}
+\section{Topological spaces}\label{form_sec_topospaces}
 
 \begin{struct}\label{topological_space}
     A topological space $X$ is a onesorted structure equipped with
diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex
index ae03273..cd85fbc 100644
--- a/library/topology/urysohn.tex
+++ b/library/topology/urysohn.tex
@@ -13,7 +13,7 @@
 \import{set/fixpoint.tex}
 \import{set/product.tex}
 
-\section{Urysohns Lemma}
+\section{Urysohns Lemma Part 1 with struct}\label{form_sec_urysohn1}
 %           In this section we want to proof Urysohns lemma. 
 %           We try to follow the proof of Klaus Jänich in his book. TODO: Book reference
 %           The Idea is to construct staircase functions as a chain.
@@ -22,7 +22,7 @@
 
 %Chains of  sets.
 
-The first tept will be a formalisation of chain constructions.
+This is the first attempt to prove Urysohns Lemma with the usage of struct. 
 
 \subsection{Chains of sets}
 %           Assume $A,B$ are subsets of a topological space $X$.
diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex
index 08841da..a1a3ba0 100644
--- a/library/topology/urysohn2.tex
+++ b/library/topology/urysohn2.tex
@@ -15,7 +15,7 @@
 \import{topology/real-topological-space.tex}
 \import{set/equinumerosity.tex}
 
-\section{Urysohns Lemma}
+\section{Urysohns Lemma}\label{form_sec_urysohn}
 
 
 
@@ -891,15 +891,25 @@
             \begin{byCase}
                 \caseOf{$x \in (\carrier[X] \setminus \closure{\at{U'}{\max{\dom{U'}}}}{X})$.}
                     Therefore $x \notin \closure{\at{U'}{\max{\dom{U'}}}}{X}$.
-                    Therefore $x \notin \closure{\at{U'}{\min{\dom{U'}}}}{X}$.
+                    We show that $x \notin \closure{\at{U'}{\min{\dom{U'}}}}{X}$.
+                    \begin{subproof}
+                        Omitted.
+                    \end{subproof}
                     Therefore $x \notin  (\closure{\at{U'}{\max{\dom{U'}}}}{X}\setminus \closure{\at{U'}{\min{\dom{U'}}}}{X})$.
-                    Then $g(x) = 1$ .
+                    We show that $g(x) = 1$.
+                    \begin{subproof}
+                        Omitted.
+                    \end{subproof}
                 \caseOf{$x \in \closure{\at{U'}{\max{\dom{U'}}}}{X}$.}
                     \begin{byCase}
                         \caseOf{$x \in \closure{\at{U'}{\min{\dom{U'}}}}{X}$.}
-                            $g(x) = \zero$.
+                            We show that $g(x) = \zero$.
+                            \begin{subproof}
+                                Omitted.
+                            \end{subproof}
                         \caseOf{$x \in  (\closure{\at{U'}{\max{\dom{U'}}}}{X}\setminus \closure{\at{U'}{\min{\dom{U'}}}}{X})$.}
                             Then $g(x)$ is the staircase step value at $x$ of $U'$ in $X$.
+                            Omitted.
                     \end{byCase}
             \end{byCase}
 
-- 
cgit v1.2.3

