working commit

4 files changed, 278 insertions, 140 deletions

diff --git a/library/nat.tex b/library/nat.tex
index ac9a141..841ac36 100644
--- a/library/nat.tex
+++ b/library/nat.tex
@@ -3,48 +3,48 @@
 
 \section{Natural numbers}
 
-\begin{abbreviation}\label{inductive_set}
+\begin{abbreviation}\label{num_inductive_set}
     $A$ is an inductive set iff $\emptyset\in A$ and for all $a\in A$ we have $\suc{a}\in A$.
 \end{abbreviation}
 
-\begin{axiom}\label{naturals_inductive_set}
+\begin{axiom}\label{num_naturals_inductive_set}
     $\naturals$ is an inductive set.
 \end{axiom}
 
-\begin{axiom}\label{naturals_smallest_inductive_set}
+\begin{axiom}\label{num_naturals_smallest_inductive_set}
     Let $A$ be an inductive set.
     Then $\naturals\subseteq A$.
 \end{axiom}
 
-\begin{abbreviation}\label{naturalnumber}
+\begin{abbreviation}\label{num_naturalnumber}
     $n$ is a natural number iff $n\in \naturals$.
 \end{abbreviation}
 
-\begin{lemma}\label{emptyset_in_naturals}
+\begin{lemma}\label{num_emptyset_in_naturals}
     $\emptyset\in\naturals$.    
 \end{lemma}
 
-\begin{signature}\label{addition_is_set}
+\begin{signature}\label{num_addition_is_set}
     $x+y$ is a set.
 \end{signature}
 
-\begin{axiom}\label{addition_on_naturals}
+\begin{axiom}\label{num_addition_on_naturals}
     $x+y$ is a natural number iff $x$ is a natural number and $y$ is a natural number.
 \end{axiom}
 
-\begin{abbreviation}\label{zero_is_emptyset}
+\begin{abbreviation}\label{num_zero_is_emptyset}
     $\zero = \emptyset$.
 \end{abbreviation}
 
-\begin{axiom}\label{addition_axiom_1}
+\begin{axiom}\label{num_addition_axiom_1}
     For all $x \in \naturals$ $x + \zero = \zero + x = x$.
 \end{axiom}
 
-\begin{axiom}\label{addition_axiom_2}
+\begin{axiom}\label{num_addition_axiom_2}
     For all $x, y \in \naturals$ $x + \suc{y} = \suc{x} + y = \suc{x+y}$.
 \end{axiom}
 
-\begin{lemma}\label{naturals_is_equal_to_two_times_naturals}
+\begin{lemma}\label{num_naturals_is_equal_to_two_times_naturals}
     $\{x+y \mid x \in \naturals, y \in \naturals \} = \naturals$.
 \end{lemma}
 
diff --git a/library/topology/real-topological-space.tex b/library/topology/real-topological-space.tex
index b2e5ea9..c76fd46 100644
--- a/library/topology/real-topological-space.tex
+++ b/library/topology/real-topological-space.tex
@@ -11,7 +11,7 @@
 \import{function.tex}
 
 
-\section{The canonical topology on $\mathbb{R}$}
+\section{Topology Reals}
 
 \begin{definition}\label{topological_basis_reals_eps_ball}
     $\topoBasisReals = \{ \epsBall{x}{\epsilon} \mid x \in \reals, \epsilon \in \realsplus\}$.
diff --git a/library/topology/urysohn.tex b/library/topology/urysohn.tex
index ff6a231..ae03273 100644
--- a/library/topology/urysohn.tex
+++ b/library/topology/urysohn.tex
@@ -36,7 +36,7 @@ The first tept will be a formalisation of chain constructions.
 %           $\overline{A_{i-1}}  \subset \interior{A_{i}}$. 
 %           In this case we call the chain legal.
 
-\begin{definition}\label{one_to_n_set}
+\begin{definition}\label{urysohnone_one_to_n_set}
     $\seq{m}{n} = \{x \in \naturals \mid  m \leq x \leq n\}$.   
 \end{definition}
 
@@ -48,7 +48,7 @@ The first tept will be a formalisation of chain constructions.
 %   together with the existence of an indexing function.
 %
 %%-----------------------
-\begin{struct}\label{sequence}
+\begin{struct}\label{urysohnone_sequence}
     A sequence $X$ is a onesorted structure equipped with
     \begin{enumerate}
         \item $\indexx$
@@ -57,8 +57,8 @@ The first tept will be a formalisation of chain constructions.
     \end{enumerate}
     such that
     \begin{enumerate}
-        \item\label{indexset_is_subset_naturals} $\indexxset[X] \subseteq \naturals$.
-        \item\label{index_is_bijection} $\indexx[X]$ is a bijection from $\indexxset[X]$ to $\carrier[X]$.
+        \item\label{urysohnone_indexset_is_subset_naturals} $\indexxset[X] \subseteq \naturals$.
+        \item\label{urysohnone_index_is_bijection} $\indexx[X]$ is a bijection from $\indexxset[X]$ to $\carrier[X]$.
     \end{enumerate}
 \end{struct}
 
@@ -67,12 +67,12 @@ The first tept will be a formalisation of chain constructions.
 
 
 
-\begin{definition}\label{cahin_of_subsets}
+\begin{definition}\label{urysohnone_cahin_of_subsets}
     $C$ is a chain of subsets iff
     $C$ is a sequence and for all $n,m \in \indexxset[C]$ such that $n < m$ we have $\indexx[C](n) \subseteq \indexx[C](m)$.
 \end{definition}
 
-\begin{definition}\label{chain_of_n_subsets}
+\begin{definition}\label{urysohnone_chain_of_n_subsets}
     $C$ is a chain of $n$ subsets iff
     $C$ is a chain of subsets and $n \in \indexxset[C]$ 
     and for all $m \in \naturals$ such that $m \leq n$ we have $m \in \indexxset[C]$.
@@ -84,7 +84,7 @@ The first tept will be a formalisation of chain constructions.
 % and also for the subproof of continuity of the limit.
 
 
-%     \begin{definition}\label{legal_chain}
+%     \begin{definition}\label{urysohnone_legal_chain}
 %         $C$ is a legal chain of subsets of $X$ iff 
 %         $C \subseteq \pow{X}$. %and 
 %         %there exist $f \in \funs{C}{\naturals}$ such that
@@ -106,49 +106,49 @@ The first tept will be a formalisation of chain constructions.
 
 \subsection{staircase function}
 
-\begin{definition}\label{minimum}
+\begin{definition}\label{urysohnone_minimum}
     $\min{X} = \{x \in X \mid \forall y \in X. x \leq y \}$.
 \end{definition}
 
-\begin{definition}\label{maximum}
+\begin{definition}\label{urysohnone_maximum}
     $\max{X} = \{x \in X \mid \forall y \in X. x \geq y \}$.
 \end{definition}
 
-\begin{definition}\label{intervalclosed}
+\begin{definition}\label{urysohnone_intervalclosed}
     $\intervalclosed{a}{b} = \{x \in \reals \mid a \leq x \leq b\}$.
 \end{definition}
 
-\begin{definition}\label{intervalopen}
+\begin{definition}\label{urysohnone_intervalopen}
     $\intervalopen{a}{b} = \{ x \in \reals \mid a < x < b\}$.
 \end{definition}
 
 
-\begin{struct}\label{staircase_function}
+\begin{struct}\label{urysohnone_staircase_function}
     A staircase function $f$ is a onesorted structure equipped with
     \begin{enumerate}
         \item $\chain$
     \end{enumerate}
     such that
     \begin{enumerate}
-        \item \label{staircase_is_function} $f$ is a function to $\intervalclosed{\zero}{1}$.
-        \item \label{staircase_domain} $\dom{f}$ is a topological space.
-        \item \label{staricase_def_chain} $C$ is a chain of subsets.
-        \item \label{staircase_chain_is_in_domain} for all $x \in C$ we have $x \subseteq \dom{f}$.
-        \item \label{staircase_behavoir_index_zero} $f(\indexx[C](1))= 1$. 
-        \item \label{staircase_behavoir_index_n} $f(\dom{f}\setminus \unions{C}) = \zero$.
-        \item \label{staircase_chain_indeset} There exist $n$ such that $\indexxset[C] = \seq{\zero}{n}$.
-        \item \label{staircase_behavoir_index_arbetrray} for all $n \in \indexxset[C]$ 
+        \item \label{urysohnone_staircase_is_function} $f$ is a function to $\intervalclosed{\zero}{1}$.
+        \item \label{urysohnone_staircase_domain} $\dom{f}$ is a topological space.
+        \item \label{urysohnone_staricase_def_chain} $C$ is a chain of subsets.
+        \item \label{urysohnone_staircase_chain_is_in_domain} for all $x \in C$ we have $x \subseteq \dom{f}$.
+        \item \label{urysohnone_staircase_behavoir_index_zero} $f(\indexx[C](1))= 1$. 
+        \item \label{urysohnone_staircase_behavoir_index_n} $f(\dom{f}\setminus \unions{C}) = \zero$.
+        \item \label{urysohnone_staircase_chain_indeset} There exist $n$ such that $\indexxset[C] = \seq{\zero}{n}$.
+        \item \label{urysohnone_staircase_behavoir_index_arbetrray} for all $n \in \indexxset[C]$ 
             such that $n \neq \zero$ we have $f(\indexx[C](n) \setminus \indexx[C](n-1)) = \rfrac{n}{ \max{\indexxset[C]} }$. 
     \end{enumerate}
 \end{struct}
 
-\begin{definition}\label{legal_staircase}
+\begin{definition}\label{urysohnone_legal_staircase}
     $f$ is a legal staircase function iff
     $f$ is a staircase function and 
     for all $n,m \in \indexxset[\chain[f]]$ such that $n \leq m$ we have $f(\indexx[\chain[f]](n)) \leq f(\indexx[\chain[f]](m))$.
 \end{definition}
 
-\begin{abbreviation}\label{urysohnspace}
+\begin{abbreviation}\label{urysohnone_urysohnspace}
     $X$ is a urysohn space iff
     $X$ is a topological space and
     for all $A,B \in \closeds{X}$ such that $A \inter B = \emptyset$
@@ -156,49 +156,49 @@ The first tept will be a formalisation of chain constructions.
     such that  $A \subseteq A'$ and $B \subseteq B'$ and $A' \inter B' = \emptyset$.    
 \end{abbreviation}
 
-\begin{definition}\label{urysohnchain}
+\begin{definition}\label{urysohnone_urysohnchain}
     $C$ is a urysohnchain in $X$ of cardinality $k$ iff %<---- TODO: cardinality unused!
     $C$ is a chain of subsets and
     for all $A \in C$ we have $A \subseteq X$ and
     for all $n,m \in \indexxset[C]$ such that $n < m$ we have $\closure{\indexx[C](n)}{X} \subseteq \interior{\indexx[C](m)}{X}$.
 \end{definition}
 
-\begin{definition}\label{urysohnchain_without_cardinality}
+\begin{definition}\label{urysohnone_urysohnchain_without_cardinality}
     $C$ is a urysohnchain in $X$ iff
     $C$ is a chain of subsets and
     for all $A \in C$ we have $A \subseteq X$ and
     for all $n,m \in \indexxset[C]$ such that $n < m$ we have $\closure{\indexx[C](n)}{X} \subseteq \interior{\indexx[C](m)}{X}$.
 \end{definition}
 
-\begin{abbreviation}\label{infinte_sequence}
+\begin{abbreviation}\label{urysohnone_infinte_sequence}
     $S$ is a infinite sequence iff $S$ is a sequence and $\indexxset[S]$ is infinite.
 \end{abbreviation}
 
-\begin{definition}\label{infinite_product}
+\begin{definition}\label{urysohnone_infinite_product}
     $X$ is the infinite product of $Y$ iff
     $X$ is a infinite sequence and for all $i \in \indexxset[X]$ we have $\indexx[X](i) = Y$.
 \end{definition}
 
-\begin{definition}\label{refinmant}
+\begin{definition}\label{urysohnone_refinmant}
     $C'$ is a refinmant of $C$ iff $C'$ is a urysohnchain in $X$
     and for all $x \in C$ we have $x \in C'$ 
     and for all $y \in C$ such that $y \subset x$ we have there exist $c \in C'$ such that $y \subset c \subset x$
     and for all $g \in C'$ such that $g \neq c$ we have not $y \subset g \subset x$.
 \end{definition}
 
-\begin{abbreviation}\label{two}
+\begin{abbreviation}\label{urysohnone_two}
     $\two = \suc{1}$.
 \end{abbreviation}
 
-\begin{lemma}\label{two_in_reals}
+\begin{lemma}\label{urysohnone_two_in_reals}
     $\two \in \reals$.
 \end{lemma}
 
-\begin{lemma}\label{two_in_naturals}
+\begin{lemma}\label{urysohnone_two_in_naturals}
     $\two \in \naturals$.
 \end{lemma}
 
-\begin{inductive}\label{power_of_two}
+\begin{inductive}\label{urysohnone_power_of_two}
     Define $\powerOfTwoSet \subseteq (\naturals \times \naturals)$.
     \begin{enumerate}
         \item  $(\zero, 1) \in \powerOfTwoSet$.
@@ -206,45 +206,45 @@ The first tept will be a formalisation of chain constructions.
     \end{enumerate}
 \end{inductive}
 
-\begin{abbreviation}\label{pot}
+\begin{abbreviation}\label{urysohnone_pot}
     $\pot = \powerOfTwoSet$.
 \end{abbreviation}
 
-\begin{lemma}\label{dom_pot}
+\begin{lemma}\label{urysohnone_dom_pot}
     $\dom{\pot} = \naturals$.
 \end{lemma}
 \begin{proof}
     Omitted.
 \end{proof}
 
-\begin{lemma}\label{ran_pot}
+\begin{lemma}\label{urysohnone_ran_pot}
     $\ran{\pot} \subseteq \naturals$.
 \end{lemma}
 
 
-\begin{axiom}\label{pot1}
+\begin{axiom}\label{urysohnone_pot1}
     $\pot \in \funs{\naturals}{\naturals}$.
 \end{axiom}
 
-\begin{axiom}\label{pot2} 
+\begin{axiom}\label{urysohnone_pot2} 
     For all $n \in \naturals$ we have there exist $k\in \naturals$ such that $(n, k) \in \powerOfTwoSet$ and $\apply{\pot}{n}=k$.
     %$\pot(n) = k$ iff there exist $x \in \powerOfTwoSet$ such that $x = (n,k)$.
 \end{axiom}
 
 
 %Without this abbreviation \pot cant be sed as a function in the standard sense
-\begin{abbreviation}\label{pot_as_function}
+\begin{abbreviation}\label{urysohnone_pot_as_function}
     $\pot(n) = \apply{\pot}{n}$.
 \end{abbreviation}
 
 %Take all points, besids one but then take all open sets not containing x but all other, so \{x\} has to be closed
-\begin{axiom}\label{hausdorff_implies_singltons_closed}
+\begin{axiom}\label{urysohnone_hausdorff_implies_singltons_closed}
     For all $X$ such that $X$ is Hausdorff we have
     for all $x \in \carrier[X]$ we have $\{x\}$ is closed in $X$.
 \end{axiom}
 
 
-\begin{lemma}\label{urysohn_set_in_between}
+\begin{lemma}\label{urysohnone_urysohn_set_in_between}
     Let $X$ be a urysohn space.
     Suppose $A,B \in \closeds{X}$.
     Suppose $A \subset B$.
@@ -284,7 +284,7 @@ The first tept will be a formalisation of chain constructions.
 \end{proof}
 
 
-\begin{proposition}\label{urysohnchain_induction_begin}
+\begin{proposition}\label{urysohnone_urysohnchain_induction_begin}
     Let $X$ be a urysohn space.
     Suppose $A,B \in \closeds{X}$.
     Suppose $A \inter B$ is empty.
@@ -347,7 +347,7 @@ The first tept will be a formalisation of chain constructions.
     
 \end{proof}
 
-\begin{proposition}\label{urysohnchain_induction_begin_step_two}
+\begin{proposition}\label{urysohnone_urysohnchain_induction_begin_step_two}
     Let $X$ be a urysohn space.
     Suppose $A,B \in \closeds{X}$.
     Suppose $A \inter B$ is empty.
@@ -364,7 +364,7 @@ The first tept will be a formalisation of chain constructions.
 
 
 
-\begin{proposition}\label{t_four_propositon}
+\begin{proposition}\label{urysohnone_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}$
     we have there exists $C \subseteq X$ such that 
@@ -376,7 +376,7 @@ The first tept will be a formalisation of chain constructions.
 
 
 
-\begin{proposition}\label{urysohnchain_induction_step_existence}
+\begin{proposition}\label{urysohnone_urysohnchain_induction_step_existence}
     Let $X$ be a urysohn space.
     Suppose $U$ is a urysohnchain in $X$.
     Then there exist $U'$ such that $U'$ is a refinmant of $U$ and $U'$ is a urysohnchain in $X$.
@@ -390,7 +390,7 @@ The first tept will be a formalisation of chain constructions.
     % such that $\closure{\indexx[U](n)}{X} \subseteq \interior{C}{X} \subseteq \closure{C}{X} \subseteq \interior{\indexx[U](n+1)}{X}$.
     
     
-    %\begin{definition}\label{refinmant}
+    %\begin{definition}\label{urysohnone_refinmant}
     %    $C'$ is a refinmant of $C$ iff for all $x \in C$ we have $x \in C'$ and 
     %    for all $y \in C$ such that $y \subset x$ 
     %    we have there exist $c \in C'$ such that $y \subset c \subset x$
@@ -404,7 +404,7 @@ The first tept will be a formalisation of chain constructions.
 
 
 
-\begin{proposition}\label{existence_of_staircase_function}
+\begin{proposition}\label{urysohnone_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$.
@@ -416,7 +416,7 @@ The first tept will be a formalisation of chain constructions.
     Omitted.
 \end{proof}
 
-\begin{abbreviation}\label{refinment_abbreviation}
+\begin{abbreviation}\label{urysohnone_refinment_abbreviation}
     $x \refine y$ iff $x$ is a refinmant of $y$.
 \end{abbreviation}
 
@@ -424,27 +424,27 @@ The first tept will be a formalisation of chain constructions.
 
 
 
-\begin{abbreviation}\label{sequence_of_functions}
+\begin{abbreviation}\label{urysohnone_sequence_of_functions}
     $f$ is a sequence of functions iff $f$ is a sequence 
     and for all $g \in \carrier[f]$ we have $g$ is a function.
 \end{abbreviation}
 
-\begin{abbreviation}\label{sequence_in_reals}
+\begin{abbreviation}\label{urysohnone_sequence_in_reals}
     $s$ is a sequence of real numbers iff $s$ is a sequence 
     and for all $r \in \carrier[s]$ we have $r \in \reals$.
 \end{abbreviation}
 
 
 
-\begin{axiom}\label{abs_behavior1}
+\begin{axiom}\label{urysohnone_abs_behavior1}
     If $x \geq \zero$ then $\abs{x} = x$.
 \end{axiom}
 
-\begin{axiom}\label{abs_behavior2}
+\begin{axiom}\label{urysohnone_abs_behavior2}
     If $x < \zero$ then $\abs{x} = \neg{x}$.
 \end{axiom}
 
-\begin{abbreviation}\label{converge}
+\begin{abbreviation}\label{urysohnone_converge}
     $s$ converges iff $s$ is a sequence of real numbers 
     and $\indexxset[s]$ is infinite
     and for all $\epsilon \in \reals$ such that $\epsilon > \zero$ we have
@@ -454,7 +454,7 @@ The first tept will be a formalisation of chain constructions.
 \end{abbreviation}
 
 
-\begin{definition}\label{limit_of_sequence}
+\begin{definition}\label{urysohnone_limit_of_sequence}
     $x$ is the limit of $s$ iff $s$ is a sequence of real numbers
     and $x \in \reals$ and 
     for all $\epsilon \in \reals$ such that $\epsilon > \zero$
@@ -463,7 +463,7 @@ The first tept will be a formalisation of chain constructions.
     we have $\abs{x - \indexx[s](n)} < \epsilon$.
 \end{definition}
 
-\begin{proposition}\label{existence_of_limit}
+\begin{proposition}\label{urysohnone_existence_of_limit}
     Let $s$ be a sequence of real numbers.
     Then $s$ converges iff there exist $x \in \reals$ 
     such that $x$ is the limit of $s$.
@@ -472,22 +472,22 @@ The first tept will be a formalisation of chain constructions.
     Omitted.
 \end{proof}
 
-\begin{definition}\label{limit_sequence}
+\begin{definition}\label{urysohnone_limit_sequence}
     $x$ is the limit sequence of $f$ iff
     $x$ is a sequence and $\indexxset[x] = \dom{f}$ and
     for all $n \in \indexxset[x]$ we have
     $\indexx[x](n) = f(n)$.
 \end{definition}
 
-\begin{definition}\label{realsminus}
+\begin{definition}\label{urysohnone_realsminus}
     $\realsminus = \{r \in \reals \mid r < \zero\}$.
 \end{definition}
 
-\begin{abbreviation}\label{realsplus}
+\begin{abbreviation}\label{urysohnone_realsplus}
     $\realsplus = \reals \setminus \realsminus$.
 \end{abbreviation}
 
-\begin{proposition}\label{intervalclosed_subseteq_reals}
+\begin{proposition}\label{urysohnone_intervalclosed_subseteq_reals}
     Suppose $a,b \in \reals$.
     Suppose $a < b$.
     Then $\intervalclosed{a}{b} \subseteq \reals$.
@@ -495,7 +495,7 @@ The first tept will be a formalisation of chain constructions.
 
 
 
-\begin{lemma}\label{fraction1}
+\begin{lemma}\label{urysohnone_fraction1}
     Let $x \in \reals$.
     Then for all $y \in \reals$ such that $x \neq y$ we have there exists $r \in \rationals$ such that $y < r < x$ or $x < r < y$.
 \end{lemma}
@@ -503,7 +503,7 @@ The first tept will be a formalisation of chain constructions.
     Omitted.
 \end{proof}
 
-\begin{lemma}\label{frection2}
+\begin{lemma}\label{urysohnone_frection2}
     Suppose $a,b \in \reals$.
     Suppose $a < b$.
     Then $\intervalopen{a}{b}$ is infinite.
@@ -512,7 +512,7 @@ The first tept will be a formalisation of chain constructions.
     Omitted.
 \end{proof}
 
-\begin{lemma}\label{frection3}
+\begin{lemma}\label{urysohnone_frection3}
     Suppose $a \in \reals$.
     Suppose $a < \zero$.
     Then there exist $N \in \naturals$ such that for all $N' \in \naturals$ such that $N' > N$ we have $\zero < \rfrac{1}{\pot(N')} < a$. 
@@ -521,7 +521,7 @@ The first tept will be a formalisation of chain constructions.
     Omitted.
 \end{proof}
 
-\begin{proposition}\label{fraction4}
+\begin{proposition}\label{urysohnone_fraction4}
     Suppose $a,b,\epsilon \in \reals$.
     Suppose $\epsilon > \zero$.
     $\abs{a - b} < \epsilon$ iff $b \in \intervalopen{(a - \epsilon)}{(a + \epsilon)}$.
@@ -530,7 +530,7 @@ The first tept will be a formalisation of chain constructions.
     Omitted.
 \end{proof}
 
-\begin{proposition}\label{fraction5}
+\begin{proposition}\label{urysohnone_fraction5}
     Suppose $a,b,\epsilon \in \reals$.
     Suppose $\epsilon > \zero$.
     $b \in \intervalopen{(a - \epsilon)}{(a + \epsilon)}$ iff $a \in \intervalopen{(b - \epsilon)}{(b + \epsilon)}$.
@@ -539,17 +539,17 @@ The first tept will be a formalisation of chain constructions.
     Omitted.
 \end{proof}
 
-\begin{proposition}\label{fraction6}
+\begin{proposition}\label{urysohnone_fraction6}
     Suppose $a,\epsilon \in \reals$.
     Suppose $\epsilon > \zero$.
     $\intervalopen{(a - \epsilon)}{(a + \epsilon)} = \{r \in \reals \mid (a - \epsilon) < r < (a + \epsilon)\} $.
 \end{proposition}
 
-\begin{abbreviation}\label{epsilonball}
+\begin{abbreviation}\label{urysohnone_epsilonball}
     $\epsBall{a}{\epsilon}  = \intervalopen{(a - \epsilon)}{(a + \epsilon)}$.
 \end{abbreviation}
 
-\begin{proposition}\label{fraction7}
+\begin{proposition}\label{urysohnone_fraction7}
     Suppose $a,\epsilon \in \reals$.
     Suppose $\epsilon > \zero$.
     Then there exist $b \in \rationals$ such that $b \in \epsBall{a}{\epsilon}$.
@@ -561,11 +561,11 @@ The first tept will be a formalisation of chain constructions.
 
 
  
-%\begin{definition}\label{sequencetwo}
+%\begin{definition}\label{urysohnone_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}
+%\begin{proposition}\label{urysohnone_sequence_existence}
 %    Suppose $N \subseteq \naturals$.
 %    Suppose $M \subseteq \naturals$.
 %    Suppose $N = M$.
@@ -586,7 +586,7 @@ The first tept will be a formalisation of chain constructions.
 
 
 
-\begin{theorem}\label{urysohn}
+\begin{theorem}\label{urysohnone_urysohn1}
     Let $X$ be a urysohn space.
     Suppose $A,B \in \closeds{X}$.
     Suppose $A \inter B$ is empty.
@@ -599,7 +599,7 @@ The first tept will be a formalisation of chain constructions.
     There exist $\eta$ such that $\carrier[\eta] = \{A, (\carrier[X] \setminus B)\}$ 
     and $\indexxset[\eta] = \{\zero, 1\}$ 
     and $\indexx[\eta](\zero) = A$
-    and $\indexx[\eta](1) = (\carrier[X] \setminus B)$  by \cref{urysohnchain_induction_begin}.
+    and $\indexx[\eta](1) = (\carrier[X] \setminus B)$  by \cref{urysohnone_urysohnchain_induction_begin}.
     
     We show that there exist $\zeta$ such that $\zeta$ is a sequence 
     and $\indexxset[\zeta] = \naturals$
@@ -919,6 +919,6 @@ The first tept will be a formalisation of chain constructions.
     %   \end{subproof}
 \end{proof}
 %
-%\begin{theorem}\label{safe}
+%\begin{theorem}\label{urysohnone_safe}
 %    Contradiction.     
 %\end{theorem}
diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex
index ce6d742..08841da 100644
--- a/library/topology/urysohn2.tex
+++ b/library/topology/urysohn2.tex
@@ -40,7 +40,7 @@
 
 
 \begin{definition}\label{chain_of_subsets}
-    $X$ is a chain of subsets in $Y$ iff $X$ is a sequence and for all $n \in \dom{X}$ we have $\at{X}{n} \subseteq \carrier[Y]$ and for all $m \in \dom{X}$ such that $m > n$ we have $\at{X}{n} \subseteq \at{X}{m}$. 
+    $X$ is a chain of subsets in $Y$ iff $X$ is a sequence and for all $n \in \dom{X}$ we have $\at{X}{n} \subseteq \carrier[Y]$ and for all $m \in \dom{X}$ such that $n < m$ we have $\at{X}{n} \subseteq \at{X}{m}$. 
 \end{definition}
 
 
@@ -49,11 +49,11 @@
 \end{definition}
 
 \begin{definition}\label{urysohn_finer_set}
-    $A$ is finer between $X$ to $Y$ in $U$ iff $\closure{X}{U} \subseteq \interior{A}{U}$ and $\closure{A}{U} \subseteq \interior{Y}{U}$.
+    $A$ is finer between $B$ to $C$ in $X$ iff $\closure{B}{X} \subseteq \interior{A}{X}$ and $\closure{A}{X} \subseteq \interior{C}{X}$.
 \end{definition}
 
 \begin{definition}\label{finer} %<-- verfeinerung 
-    $Y$ is finer then $X$ in $U$ iff for all $n \in \dom{X}$ we have $\at{X}{n} \in \ran{Y}$ and for all $m \in \dom{X}$ such that $n < m$ we have there exist $k \in \dom{Y}$ such that $\at{Y}{k}$ is finer between $\at{X}{n}$ to $\at{X}{m}$ in $U$.
+    $A$ is finer then $B$ in $X$ iff for all $n \in \dom{B}$ we have $\at{B}{n} \in \ran{A}$ and for all $m \in \dom{B}$ such that $n < m$ we have there exist $k \in \dom{A}$ such that $\at{A}{k}$ is finer between $\at{B}{n}$ to $\at{B}{m}$ in $X$.
 \end{definition}
 
 \begin{definition}\label{follower_index}
@@ -92,6 +92,46 @@
     $f$ is consistent on $X$ to $Y$ iff $f$ is a bijection from $\dom{X}$ to $\dom{Y}$ and for all $n,m \in \dom{X}$ such that $n < m$ we have $f(n) < f(m)$.
 \end{definition}
 
+
+%\begin{definition}\label{staircase}
+%    $f$ is a staircase function adapted to $U$ in $X$ iff $U$ is a urysohnchain of $X$ and $f$ is a function from $\carrier[X]$ to $\reals$ and there exist $k \in \naturals$ such that $k = \max{\dom{U}}$ and for all $x,y \in \carrier[X]$ such that $y \in \carrier[X] \setminus \at{U}{k}$ and $x \in \at{U}{k}$ we have $f(y) = 1$ and there exist $n,m \in \dom{U}$ such that $n$ follows $m$ in $\dom{U}$ and $x \in (\at{U}{m} \setminus \at{U}{n})$ and $f(x)= \rfrac{m}{k}$.
+%\end{definition}
+
+
+\begin{definition}\label{staircase_step_value1}
+    $a$ is the staircase step value at $y$ of $U$ in $X$ iff there exist $n,m \in \dom{U}$ such that $n$ follows $m$ in $\dom{U}$ and $y \in \closure{\at{U}{n}}{X} \setminus \closure{\at{U}{m}}{X}$ and $a = \rfrac{n}{\max{\dom{U}}}$.
+\end{definition}
+
+\begin{definition}\label{staircase_step_value2}
+    $a$ is the staircase step valuetwo at $y$ of $U$ in $X$ iff either if $y \in (\carrier[X] \setminus \closure{\at{U}{\max{\dom{U}}}}{X})$ then $a = 1$ or $a$ is the staircase step valuethree at $y$ of $U$ in $X$.
+\end{definition}
+
+\begin{definition}\label{staircase_step_value3}
+    $a$ is the staircase step valuethree at $y$ of $U$ in $X$ iff if $y \in \closure{\at{U}{\min{\dom{U}}}}{X}$ then $f(z) = \zero$.
+\end{definition}
+
+
+\begin{definition}\label{staircase2}
+    $f$ is a staircase function adapted to $U$ in $X$ iff $U$ is a urysohnchain of $X$ and $f$ is a function from $\carrier[X]$ to $\reals$ and for all $y \in \carrier[X]$ we have either $f(y)$ is the staircase step value at $y$ of $U$ in $X$ or $f(y)$ is the staircase step valuetwo at $y$ of $U$ in $X$.
+\end{definition}
+
+\begin{definition}\label{staircase_sequence}
+    $S$ is staircase sequence of $U$ in $X$ iff $S$ is a sequence and $U$ is a lifted urysohnchain of $X$ and $\dom{U} = \dom{S}$ and for all $n \in \dom{U}$ we have $\at{S}{n}$ is a staircase function adapted to $\at{U}{n}$ in $X$.
+\end{definition}
+
+\begin{definition}\label{staircase_limit_point}
+    $x$ is the staircase limit of $S$ with $y$ iff $x \in \reals$ and for all $\epsilon \in \realsplus$ there exist $n_0 \in \naturals$ such that for all $n \in \naturals$ such that $n_0 \rless n$ we have $\apply{\at{S}{n}}{y} \in \epsBall{x}{\epsilon}$.
+\end{definition}
+
+%\begin{definition}\label{staircase_limit_function}
+%    $f$ is a limit function of a staircase $S$ iff $S$ is staircase sequence of $U$ and $U$ is a lifted urysohnchain of $X$ and $\dom{f} = \carrier[X]$ and for all $x \in \dom{f}$ we have $f(x)$ is the staircase limit of $S$ with $x$ and $f$ is a function from $\carrier[X]$ to $\reals$.
+%\end{definition}
+%
+\begin{definition}\label{staircase_limit_function}
+    $f$ is the limit function of staircase $S$ together with $U$ and $X$ iff $S$ is staircase sequence of $U$ in $X$ and $U$ is a lifted urysohnchain of $X$ and $\dom{f} = \carrier[X]$ and for all $x \in \dom{f}$ we have $f(x)$ is the staircase limit of $S$ with $x$ and $f$ is a function from $\carrier[X]$ to $\reals$.
+\end{definition}
+
+
 \begin{proposition}\label{naturals_in_transitive}
     $\naturals$ is a \in-transitive set.
 \end{proposition}
@@ -659,33 +699,26 @@
 \end{proof}
 
 
-\begin{definition}\label{staircase}
-    $f$ is a staircase function adapted to $U$ in $X$ iff $U$ is a urysohnchain of $X$ and for all $x,n,m,k$ such that $k = \max{\dom{U}}$ and $n,m \in \dom{U}$ and $n$ follows $m$ in $\dom{U}$ and $x \in (\at{U}{m} \setminus \at{U}{n})$ we have $f(x)= \rfrac{m}{k}$.
-\end{definition}
-
-\begin{definition}\label{staircase_sequence}
-    $S$ is staircase sequence of $U$ iff $S$ is a sequence and $U$ is a lifted urysohnchain of $X$ and $\dom{U} = \dom{S}$ and for all $n \in \dom{U}$ we have $\at{S}{n}$ is a staircase function adapted to $\at{U}{n}$ in $U$.
-\end{definition}
-
-\begin{definition}\label{staircase_limit_point}
-    $x$ is the staircase limit of $S$ with $y$ iff $x \in \reals$ and for all $\epsilon \in \realsplus$ there exist $n_0 \in \naturals$ such that for all $n \in \naturals$ such that $n_0 \rless n$ we have $\apply{\at{S}{n}}{y} \in \epsBall{x}{\epsilon}$.
-\end{definition}
-
-\begin{definition}\label{staircase_limit_function}
-    $f$ is a limit function of a staircase $S$ iff $S$ is staircase sequence of $U$ and $U$ is a lifted urysohnchain of $X$ and $\dom{f} = \carrier[X]$ and for all $x \in \dom{f}$ we have $f(x)$ is the staircase limit of $S$ with $x$ and $f$ is a function from $\carrier[X]$ to $\reals$.
-\end{definition}
+\begin{proposition}\label{staircase_ran_in_zero_to_one}
+    Let $X$ be a urysohn space.
+    Suppose $U$ is a urysohnchain of $X$.
+    Suppose $f$ is a staircase function adapted to $U$ in $X$.
+    Then $\ran{f} \subseteq \intervalclosed{\zero}{1}$.
+\end{proposition}
+\begin{proof}
+    Omitted.
+\end{proof}
 
-%\begin{definition}\label{staircase_limit_function}
-%    $f$ is a limit function of staircase $S$ iff $S$ is staircase sequence of $U$ and $U$ is a lifted urysohnchain of $X$ and $\dom{f} = \carrier[X]$ and for all $x \in \dom{f}$ we have $f(x)$ is the staircase limit of $S$ with $x$ and $f$ is a function from $\carrier[X]$ to $\reals$.
-%\end{definition}
-%
-%\begin{proposition}\label{staircase_limit_is_continuous}
-%    Suppose $X$ is a urysohnspace.
-%    Suppose $U$ is a lifted urysohnchain of $X$.
-%    Suppose $S$ is staircase sequence of $U$.
-%    Suppose $f$ is the limit function of a staircase $S$.
-%    Then $f$ is continuous.
-%\end{proposition}
+\begin{proposition}\label{staircase_limit_is_continuous}
+    Let $X$ be a urysohn space.
+    Suppose $U$ is a lifted urysohnchain of $X$.
+    Suppose $S$ is staircase sequence of $U$ in $X$.
+    Suppose $f$ is the limit function of staircase $S$ together with $U$ and $X$.
+    Then $f$ is continuous.
+\end{proposition}
+\begin{proof}
+    Omitted.
+\end{proof}
 
 \begin{theorem}\label{urysohnsetinbeetween}
     Let $X$ be a urysohn space.
@@ -712,8 +745,26 @@
     Omitted.
 \end{proof}
 
+\begin{lemma}\label{fractions_between_zero_one}
+    Suppose $n,m \in \naturals$.
+    Suppose $m > n$.
+    Then $\zero \leq \rfrac{n}{m} \leq 1$.
+\end{lemma}
+\begin{proof}
+    Omitted.
+\end{proof}
 
+\begin{lemma}\label{intervalclosed_border_is_elem}
+    Suppose $a,b \in \reals$.
+    Suppose $a < b$.
+    Then $a,b \in \intervalclosed{a}{b}$.  
+\end{lemma}
 
+\begin{lemma}\label{urysohnchain_subseteqrel}
+    Let $X$ be a urysohn space.
+    Suppose $U$ is a urysohnchain of $X$.
+    Then for all $n,m \in \dom{U}$ such that $n < m$ we have $\at{U}{n} \subseteq \at{U}{m}$.
+\end{lemma}
 
 
 \begin{theorem}\label{urysohn}
@@ -721,8 +772,8 @@
     Suppose $A,B \in \closeds{X}$.
     Suppose $A \inter B$ is empty.
     Suppose $\carrier[X]$ is inhabited.
-    There exist $f$ such that $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ 
-    and $f(A) = \zero$ and $f(B)= 1$ and $f$ is continuous.
+    There exist $f$ such that $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ and $f$ is continuous
+    and for all $a,b$ such that $a \in A$ and $b \in B$ we have $f(a)= \zero$ and $f(b) = 1$.
 \end{theorem}
 \begin{proof}
     Let $X' = \carrier[X]$.
@@ -796,46 +847,133 @@
     \end{subproof}
     Take $U$ such that $U$ is a lifted urysohnchain of $X$ and $\at{U}{\zero} = U_0$.
 
-    We show that there exist $S$ such that $S$ is staircase sequence of $U$.
+    We show that there exist $S$ such that $S$ is staircase sequence of $U$ in $X$.
     \begin{subproof}
         Omitted.
     \end{subproof}
-    Take $S$ such that $S$ is staircase sequence of $U$.
+    Take $S$ such that $S$ is staircase sequence of $U$ in $X$.
 
     %For all $x \in \carrier[X]$ we have there exist $r,R$ such that $r \in \reals$ and $R$ is a sequence of reals and $\dom{R} = \naturals$ and $R$ converge to $r$ and for all $n \in \naturals$ we have $\at{R}{n} = \apply{\at{S}{n}}{x}$.
 %
     %We show that for all $x \in \carrier[X]$ there exists $r \in \intervalclosed{a}{b}$ such that for .
-%
+    We show that there exist $f$ such that $f$ is the limit function of staircase $S$ together with $U$ and $X$.
+    \begin{subproof}
+        Omitted.
+    \end{subproof}
+    Take $f$ such that $f$ is the limit function of staircase $S$ together with $U$ and $X$.
+    Then $f$ is continuous.
+    We show that $\dom{f} = \carrier[X]$.
+    \begin{subproof}
+        Trivial.
+    \end{subproof}
+    $f$ is a function.
+    We show that $\ran{f} \subseteq \intervalclosed{\zero}{1}$.
+    \begin{subproof}
+        It suffices to show that $f$ is a function to $\intervalclosed{\zero}{1}$.
+        It suffices to show that for all $x \in \dom{f}$ we have $f(x) \in \intervalclosed{\zero}{1}$.
+        Fix $x \in \dom{f}$.
+        $f(x)$ is the staircase limit of $S$ with $x$.
+        Therefore $f(x) \in \reals$.
+        
+        We show that for all $n \in \naturals$ we have $\apply{\at{S}{n}}{x} \in \intervalclosed{\zero}{1}$.
+        \begin{subproof}
+            Fix $n \in \naturals$.
+            Let $g = \at{S}{n}$.
+            Let $U' = \at{U}{n}$.
+            $\at{S}{n}$ is a staircase function adapted to $\at{U}{n}$ in $X$.
+            $g$ is a staircase function adapted to $U'$ in $X$.
+            $U'$ is a urysohnchain of $X$.
+            $g$ is a function from $\carrier[X]$ to $\reals$.
+            It suffices to show that $\ran{g} \subseteq \intervalclosed{\zero}{1}$ by \cref{function_apply_default,reals_axiom_zero_in_reals,intervalclosed,one_is_positiv,function_apply_elim,inter,inter_absorb_supseteq_left,ran_iff,funs_is_relation,funs_is_function,staircase2}.
+            It suffices to show that for all $x \in \dom{g}$ we have $g(x) \in \intervalclosed{\zero}{1}$.
+            Fix $x\in \dom{g}$.
+            Then $x \in \carrier[X]$.
+            \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}$.
+                    Therefore $x \notin  (\closure{\at{U'}{\max{\dom{U'}}}}{X}\setminus \closure{\at{U'}{\min{\dom{U'}}}}{X})$.
+                    Then $g(x) = 1$ .
+                \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$.
+                        \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$.
+                    \end{byCase}
+            \end{byCase}
+
+            
+
+            %$\at{S}{n}$ is a staircase function adapted to $\at{U}{n}$ in $X$.
+            %$\at{U}{n}$ is a urysohnchain of $X$.
+            %$\at{S}{n}$ is a function from $\carrier[X]$ to $\reals$.
+            %there exist $k \in \naturals$ such that $k = \max{\dom{\at{U}{n}}}$.
+            %Take $k \in \naturals$ such that $k = \max{\dom{\at{U}{n}}}$.
+            %\begin{byCase}
+            %    \caseOf{$x \in \carrier[X] \setminus \at{\at{U}{n}}{k}$.}
+            %        $1 \in \intervalclosed{\zero}{1}$.
+            %        We show that for all $y \in (\carrier[X] \setminus \at{\at{U}{n}}{k})$ we have $\apply{\at{S}{n}}{y} = 1$.
+            %        \begin{subproof}
+            %            Omitted.
+            %        \end{subproof}
+            %        Then $\apply{\at{S}{n}}{x} = 1$.
+            %    \caseOf{$x \notin \carrier[X] \setminus \at{\at{U}{n}}{k}$.}
+            %        %There exist $n',m' \in \dom{\at{U}{n}}$ such that $n'$ follows $m'$ in $\dom{\at{U}{n}}$ and $x \in (\at{\at{U}{n}}{n'} \setminus \at{\at{U}{n}}{m'})$.
+            %        Take $n',m' \in \dom{\at{U}{n}}$ such that $n'$ follows $m'$ in $\dom{\at{U}{n}}$ and $x \in (\at{\at{U}{n}}{n'} \setminus \at{\at{U}{n}}{m'})$.
+            %        Then  $\apply{\at{S}{n}}{x} = \rfrac{m'}{k'}$.
+            %        It suffices to show that $\rfrac{m'}{k'} \in \intervalclosed{\zero}{1}$.
+            %        $\zero \leq m' \leq k$.
+            %\end{byCase}
+            %%It suffices to show that $\zero \leq \apply{\at{S}{n}}{x} \leq 1$.
+            %%It suffices to show that $\ran{\at{S}{n}} \subseteq \intervalclosed{\zero}{1}$.
+        \end{subproof}
+
+        Suppose not.
+        Then $f(x) < \zero$ or $f(x) > 1$ by \cref{reals_order_total,reals_axiom_zero_in_reals,intervalclosed,one_is_positiv,one_in_reals}.
+        For all $\epsilon \in \realsplus$ we have there exist $m \in \naturals$ such that $\apply{\at{S}{m}}{x} \in \epsBall{f(x)}{\epsilon}$ by \cref{plus_one_order,naturals_is_equal_to_two_times_naturals,subseteq,naturals_subseteq_reals,staircase_limit_point}.
+        \begin{byCase}
+            \caseOf{$f(x) < \zero$.}
+                Let $\delta = \zero - f(x)$.
+                $\delta \in \realsplus$.
+                It suffices to show that for all $n \in \naturals$ we have $\apply{\at{S}{n}}{x} \notin \epsBall{f(x)}{\delta}$.
+                Fix $n \in \naturals$.
+                $\at{S}{n}$ is a staircase function adapted to $\at{U}{n}$ in $X$.
+                For all $y \in \epsBall{f(x)}{\delta}$ we have $y < \zero$ by \cref{epsilon_ball,minus_behavior1,minus_behavior3,minus,apply,intervalopen}.
+                It suffices to show that $\apply{\at{S}{n}}{x} \in \intervalclosed{\zero}{1}$.
+                Trivial.
+            \caseOf{$f(x) > 1$.}
+                Let $\delta = f(x) - 1$.
+                $\delta \in \realsplus$.
+                It suffices to show that for all $n \in \naturals$ we have $\apply{\at{S}{n}}{x} \notin \epsBall{f(x)}{\delta}$.
+                Fix $n \in \naturals$.
+                $\at{S}{n}$ is a staircase function adapted to $\at{U}{n}$ in $X$.
+                For all $y \in \epsBall{f(x)}{\delta}$ we have $y > 1$ by \cref{epsilon_ball,reals_addition_minus_behavior2,minus_in_reals,apply,reals_addition_minus_behavior1,minus,reals_add,realsplus_in_reals,one_in_reals,reals_axiom_kommu,intervalopen}.
+                It suffices to show that $\apply{\at{S}{n}}{x} \in \intervalclosed{\zero}{1}$.
+                Trivial.
+        \end{byCase}
+
+    \end{subproof}
+    Therefore $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ by \cref{staircase_limit_function,surj_to_fun,fun_to_surj,neq_witness,inters_of_ordinals_elem,times_tuple_elim,img_singleton_iff,foundation,subseteq_emptyset_iff,inter_eq_left_implies_subseteq,inter_emptyset,funs_intro,fun_ran_iff,not_in_subseteq}.
+
+    We show that for all $a \in A$ we have $f(a) = \zero$.
+    \begin{subproof}
+        Omitted.
+    \end{subproof}
+    We show that for all $b \in B$ we have $f(b) = 1$.
+    \begin{subproof}
+        Omitted.
+    \end{subproof}
+
 
-    
 \end{proof}
 
-\begin{theorem}\label{safe}
-    Contradiction.     
-\end{theorem}
+%\begin{theorem}\label{safe}
+%    Contradiction.     
+%\end{theorem}
 
 
 
 
 
-%
-%Ideen:
-%Eine folge ist ein Funktion mit domain \subseteq Natürlichenzahlen. als predicat
-%
-%zulässig und verfeinerung von ketten als predicat definieren. 
-%
-%limits und punkt konvergenz als prädikat.
-%
-%
-%Vor dem Beweis vor dem eigentlichen Beweis.
-%die abgeleiteten Funktionen
-%
-%\derivedstiarcasefunction on A
-%
-%abbreviation: \at{f}{n} = f_{n}
-%
-%
-%TODO:
-%Reals ist ein topologischer Raum
-%