Abgabe

Submission of Formalisation

35 files changed, 3863 insertions, 227 deletions

diff --git a/latex/naproche.sty b/latex/naproche.sty
index 476d3dd..c0fd318 100644
--- a/latex/naproche.sty
+++ b/latex/naproche.sty
@@ -40,6 +40,7 @@
 \newtheorem{remark}[theoremcount]{Remark}
 \newtheorem{signature}[theoremcount]{Signature}
 \newtheorem{theorem}[theoremcount]{Theorem}
+\newtheorem{inductive}[theoremcount]{Inductive}
 
 % Theorem environments without numbering.
 \newtheorem*{quotedaxiom}{Axiom}
@@ -100,6 +101,7 @@
 \newcommand{\memrel}[1]{{\in_{#1}}}
 \newcommand{\monusNat}{-_{\naturals}}
 \newcommand{\naturals}{\mathcal{N}}
+\newcommand{\naturalsPlus}{\mathcal{N}_{+}}
 \newcommand{\notmeets}{\mathrel{\not\meets}}
 \newcommand{\pow}[1]{\fun{Pow}(#1)}
 \newcommand{\precedes}{<}
@@ -132,6 +134,30 @@
 \newcommand{\integers}{\mathcal{Z}}
 \newcommand{\zero}{0}
 \newcommand{\one}{1}
+\newcommand{\rmul}{\cdot}
+\newcommand{\inv}[1]{#1^{-1}}
+\newcommand{\rfrac}[2]{\frac{#1}{#2}}
+\newcommand{\rationals}{\mathcal{Q}}
+\newcommand{\rminus}{-_{\mathcal{R}}}
+\newcommand{\seq}[2]{\{#1, ... ,#2\}}
+\newcommand{\indexx}[2][]{index_{#1}(#2)}
+\newcommand{\indexxset}[1]{#1}
+\newcommand{\topoBasisReals}{\mathbb{B}_{\mathcal{R}}}
+\newcommand{\intervalopen}[2]{(#1, #2)}
+\newcommand{\intervalclosed}[2]{[#1, #2]}
+\newcommand{\epsBall}[2]{\mathcal{B}_{#1,#2}}
+\newcommand{\realsplus}{\reals_{+}}
+\newcommand{\rless}{<}
+\newcommand{\two}{2}
+\newcommand{\powerOfTwoSet}{\mathbb{P}_{2^{}}}
+\newcommand{\pot}{\powerOfTwoSet}
+\newcommand{\chain}[1]{#1}
+\newcommand{\refine}{\text{ finer than }}
+\newcommand{\abs}[1]{\left\lvert#1\right\rvert}
+\newcommand{\realsminus}{\reals_{-}}
+\newcommand{\at}[2]{#1(#2)}
+\newcommand{\intervalopenInfiniteLeft}[1]{(-\infty, #1)}
+\newcommand{\intervalopenInfiniteRight}[1]{(#1, \infty)}
 
 
 \newcommand\restrl[2]{{% we make the whole thing an ordinary symbol
@@ -165,6 +191,7 @@
 \newcommand{\closure}[2]{\fun{cl}_{#2}{#1}}
 \newcommand{\frontier}[2]{\fun{fr}_{#2}{#1}}
 \newcommand{\neighbourhoods}[2]{\textsf{N}_{#2}{#1}}
+\newcommand{\neighbourhoodsSet}[2]{\textsf{N}_{SET #2}{#1}}
 \newcommand{\disconnections}[1]{\fun{Disconnections}{#1}}
 
 \newcommand{\teezero}{\ensuremath{T_0}} % Kolmogorov
diff --git a/latex/stdlib.tex b/latex/stdlib.tex
index dba42a2..9879708 100644
--- a/latex/stdlib.tex
+++ b/latex/stdlib.tex
@@ -46,4 +46,8 @@
     \input{../library/topology/basis.tex}
     \input{../library/topology/disconnection.tex}
     \input{../library/numbers.tex}
+    \input{../library/topology/urysohn.tex}
+    \input{../library/topology/urysohn2.tex}
+    \input{../library/topology/real-topological-space.tex}
+    %\input{../library/wunschzettel.tex}
 \end{document}
diff --git a/library/algebra/group.tex b/library/algebra/group.tex
index a79bd2f..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
@@ -80,3 +80,13 @@
 \begin{definition}\label{group_automorphism}
     Let $f$ be a function. $f$ is a group-automorphism iff $G$ is a group and $\dom{f}=G$ and $\ran{f}=G$. 
 \end{definition}
+
+\begin{definition}\label{trivial_group}
+    $G$ is the trivial group iff $G$ is a group and $\{\neutral[G]\}=G$.
+\end{definition}
+
+\begin{theorem}\label{trivial_implies_abelian}
+    Let $G$ be a group.
+    Suppose $G$ is the trivial group.
+    Then $G$ is an abelian group.
+\end{theorem}
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 d0dec59..5682619 100644
--- a/library/cardinal.tex
+++ b/library/cardinal.tex
@@ -1,8 +1,9 @@
-\section{Cardinality}
+\section{Cardinality}\label{form_sec_cardinality}
 
 \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,10 @@
 \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}
+
+
diff --git a/library/everything.tex b/library/everything.tex
index 783679f..94dd6d8 100644
--- a/library/everything.tex
+++ b/library/everything.tex
@@ -30,11 +30,12 @@
 \import{topology/disconnection.tex}
 \import{topology/separation.tex}
 \import{numbers.tex}
+\import{topology/urysohn2.tex}
 
 \begin{proposition}\label{trivial}
     $x = x$.
 \end{proposition}
 
-%\begin{proposition}\label{safe}
-%    Contradiction.
-%\end{proposition}
+\begin{proposition}\label{safe}
+    Contradiction.
+\end{proposition}
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/numbers.tex b/library/numbers.tex
index 1837ae8..d3af3f1 100644
--- a/library/numbers.tex
+++ b/library/numbers.tex
@@ -1,7 +1,10 @@
 \import{order/order.tex}
 \import{relation.tex}
+\import{set/suc.tex}
+\import{ordinal.tex}
 
-\section{The real numbers}
+
+\section{The numbers}\label{form_sec_numbers}
 
 \begin{signature}
     $\reals$ is a set.
@@ -15,7 +18,19 @@
     $x \rmul y$ is a set.
 \end{signature}
 
-\subsection{Basic axioms of the reals}
+
+
+\subsection{Creation of natural numbers}
+
+\subsubsection{Defenition and axioms}
+
+\begin{abbreviation}\label{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{abbreviation}\label{zero_is_emptyset}
+    $\zero = \emptyset$.
+\end{abbreviation}
 
 \begin{axiom}\label{reals_axiom_zero_in_reals}
     $\zero \in \reals$.
@@ -29,43 +44,354 @@
     $\zero \neq 1$.
 \end{axiom}
 
-\begin{definition}\label{reals_definition_order_def}
-    $x < y$ iff there exist $z \in \reals$ such that $x + (z \rmul z) = y$.
-\end{definition}
+\begin{axiom}\label{one_is_suc_zero}
+    $\suc{\zero} = 1$.
+\end{axiom}
 
-%\begin{axiom}\label{reals_axiom_order}
-%    $\lt[\reals]$ is an order on $\reals$.
-%\end{axiom}
+\begin{axiom}\label{naturals_subseteq_reals}
+    $\naturals \subseteq \reals$.
+\end{axiom}
 
-%\begin{abbreviation}\label{lesseq_on_reals}
-%    $x \leq y$ iff $(x,y) \in \lt[\reals]$.
-%\end{abbreviation}
+\begin{axiom}\label{naturals_inductive_set}
+    $\naturals$ is an inductive set.
+\end{axiom}
 
-\begin{abbreviation}\label{less_on_reals}
-    $x \leq y$ iff it is wrong that $y < x$.
-\end{abbreviation}
+\begin{axiom}\label{naturals_smallest_inductive_set}
+    Let $A$ be an inductive set.
+    Then $\naturals\subseteq A$.
+\end{axiom}
 
-\begin{abbreviation}\label{greater_on_reals}
-    $x > y$ iff $y \leq x$.
+\begin{abbreviation}\label{is_a_natural_number}
+    $n$ is a natural number iff $n \in \naturals$.
 \end{abbreviation}
 
-\begin{abbreviation}\label{greatereq_on_reals}
-    $x \geq y$ iff it is wrong that $x < y$.
-\end{abbreviation}
+\begin{axiom}\label{naturals_addition_axiom_1}
+    For all $n \in \naturals$ $n + \zero = \zero + n = n$.
+\end{axiom}
 
-\begin{axiom}\label{reals_axiom_dense}
-    For all $x,y \in \reals$ if $x < y$ then 
-    there exist $z \in \reals$ such that $x < z$ and $z < y$.
+\begin{axiom}\label{naturals_addition_axiom_2}
+    For all $n, m \in \naturals$ $n + \suc{m} = \suc{n} + m = \suc{n+m}$.
 \end{axiom}
 
-\begin{axiom}\label{reals_axiom_assoc}
-    For all $x,y,z \in \reals$ $(x + y) + z = x + (y + z)$ and $(x \rmul y) \rmul z = x \rmul (y \rmul z)$.
+\begin{axiom}\label{naturals_mul_axiom_1}
+    For all $n \in \naturals$ we have $n \rmul \zero = \zero = \zero \rmul n$.
+\end{axiom}
+
+\begin{axiom}\label{naturals_mul_axiom_2}
+    For all $n,m \in \naturals$ we have $\suc{n} \rmul m = (n \rmul m) + m$.
+\end{axiom}
+
+\begin{axiom}\label{addition_on_naturals}
+    If $x$ is a natural number and $y$ is a natural number then $x+y$ is a natural number.
 \end{axiom}
 
+\begin{axiom}\label{naturals_rmul_is_closed_in_n}
+    For all $n,m \in \naturals$ we have $(n \rmul m) \in \naturals$.
+\end{axiom}
+
+\begin{axiom}\label{naturals_add_is_closed_in_n}
+    For all $n,m \in \naturals$ we have $(n + m) \in \naturals$.
+\end{axiom}
+
+\subsubsection{Natural numbers as ordinals}
+
+
+\begin{lemma}\label{nat_is_successor_ordinal}
+    Let $n\in\naturals$.
+    Suppose $n\neq \emptyset$.
+    Then $n$ is a successor ordinal.
+\end{lemma}
+\begin{proof}
+    Let $M = \{ m\in \naturals \mid\text{$m = \emptyset$ or $m$ is a successor ordinal}\}$.
+    $M$ is an inductive set by \cref{suc_ordinal,naturals_inductive_set,successor_ordinal,emptyset_is_ordinal}.
+    Now $M\subseteq \naturals\subseteq M$
+        by \cref{subseteq,naturals_smallest_inductive_set}.
+    Thus $M = \naturals$.
+    Follows by \cref{subseteq}.
+\end{proof}
+
+\begin{lemma}\label{nat_is_transitiveset}
+    $\naturals$ is \in-transitive.
+\end{lemma}
+\begin{proof}
+    Let $M = \{ m\in\naturals \mid \text{for all $n\in m$ we have $n\in\naturals$} \}$.
+    $\emptyset\in M$.
+    For all $n\in M$ we have $\suc{n}\in M$
+        by \cref{naturals_inductive_set,suc}.
+    Thus $M$ is an inductive set.
+    Now $M\subseteq \naturals\subseteq M$
+        by \cref{subseteq,naturals_smallest_inductive_set}.
+    Hence $\naturals = M$.
+\end{proof}
+
+\begin{lemma}\label{natural_number_is_ordinal}
+    Every natural number is an ordinal.
+\end{lemma}
+\begin{proof}
+    Follows by \cref{suc_ordinal,suc_neq_emptyset,naturals_inductive_set,nat_is_successor_ordinal,successor_ordinal,suc_ordinal_implies_ordinal}.
+\end{proof}
+
+\begin{lemma}\label{omega_is_an_ordinal}
+    $\naturals$ is an ordinal.
+\end{lemma}
+\begin{proof}
+    Follows by \cref{natural_number_is_ordinal,transitive_set_of_ordinals_is_ordinal,nat_is_transitiveset}.
+\end{proof}
+
+\begin{lemma}\label{omega_is_a_limit_ordinal}
+    $\naturals$ is a limit ordinal.
+\end{lemma}
+\begin{proof}
+    $\emptyset\precedes \naturals$.
+    If $n\in \naturals$, then $\suc{n}\in\naturals$.
+\end{proof}
+
+
+\subsubsection{Properties and Facts natural numbers}
+
+\begin{theorem}\label{induction_principle}
+    Let $P$ be a set.
+    Suppose $P \subseteq \naturals$.
+    Suppose $\zero \in P$.
+    Suppose $\forall n \in P. \suc{n} \in P$.
+    Then $P = \naturals$.
+\end{theorem}
+\begin{proof}
+    Trivial.
+\end{proof}
+
+\begin{proposition}\label{existence_of_suc}
+    Let $n \in \naturals$.
+    Suppose $n \neq \zero$.
+    Then there exist $n' \in \naturals$ such that $\suc{n'} = n$.
+\end{proposition}
+\begin{proof}
+    Follows by \cref{transitiveset,nat_is_transitiveset,suc_intro_self,successor_ordinal,nat_is_successor_ordinal}.
+\end{proof}
+
+\begin{proposition}\label{suc_eq_plus_one}
+    Let $n \in \naturals$.
+    Then $\suc{n} = n + 1$.
+\end{proposition}
+\begin{proof}
+    Let $P = \{ n \in \naturals \mid n + 1 = 1 + n  \}$.
+    $\zero \in P$.
+    It suffices to show that if $m \in P$ then $\suc{m} \in P$.
+\end{proof}
+
+\begin{proposition}\label{naturals_1_kommu}
+    Let $n \in \naturals$.
+    Then $1 + n = n + 1$.
+\end{proposition}
+\begin{proof}
+    Follows by \cref{suc_eq_plus_one,naturals_addition_axiom_2,naturals_addition_axiom_1,naturals_inductive_set,one_is_suc_zero}.
+\end{proof}
+
+\begin{proposition}\label{naturals_add_kommu}
+    For all $n \in \naturals$ we have for all $m\in \naturals$ we have $n + m = m + n$.
+\end{proposition}
+\begin{proof}
+    Fix $n \in \naturals$.
+    Let $P = \{ m \in \naturals \mid m + n = n + m \}$.
+    It suffices to show that $P = \naturals$.
+    $P \subseteq \naturals$.
+    $\zero \in P$.
+    It suffices to show that if $m \in P$ then $\suc{m} \in P$.
+\end{proof}
+
+\begin{proposition}\label{naturals_add_assoc}
+    Suppose $n,m,k \in \naturals$.
+    Then $n + (m + k) = (n + m) + k$.
+\end{proposition}
+\begin{proof}
+    Let $P = \{ k \in \naturals \mid \text{for all $n',m' \in \naturals$ we have $n' + (m' + k) = (n' + m') + k$}\}$.
+    $P \subseteq \naturals$.
+    $\zero \in P$.
+    It suffices to show that for all $k \in P$ we have $\suc{k} \in P$.
+    Fix $k \in P$.
+    It suffices to show that for all $n' \in \naturals$ we have for all $m' \in \naturals$ we have $n' + (m' + \suc{k}) = (n' + m') + \suc{k}$.
+    Fix $n' \in \naturals$.
+    Fix $m' \in \naturals$.
+    \begin{align*}
+        (n' + m') + \suc{k}    \\
+        &= \suc{(n' + m') + k}   \\
+        &= \suc{n' + (m' + k)} \\
+        &= n' + \suc{(m' + k)} \\
+        &= n' + (m' + \suc{k})
+    \end{align*}
+\end{proof}
+
+\begin{proposition}\label{naturals_rmul_one_left}
+    For all $n \in \naturals$ we have $1 \rmul n = n$.
+\end{proposition}
+\begin{proof}
+    Fix $n \in \naturals$.
+    \begin{align*}
+        1 \rmul n  \\
+        &= \suc{\zero} \rmul n \\
+        &= (\zero \rmul n) + n \\
+        &= (\zero) + n \\
+        &= n
+    \end{align*}
+\end{proof}
+
+\begin{proposition}\label{naturals_add_remove_brakets}
+    Suppose $n,m,k \in \naturals$.
+    Then $(n + m) + k = n + m + k = n + (m + k)$.    
+\end{proposition}
+
+\begin{proposition}\label{naturals_add_remove_brakets2}
+    Suppose $n,m,k,l \in \naturals$.
+    Then $(n + m) + (k + l)= n + m + k + l = n + (m + k) + l = (((n + m) + k) + l)$.    
+\end{proposition}
+
+%\begin{proposition}\label{natural_disstro_oneline}
+%    Suppose $n,m,k \in \naturals$.
+%    Then $n \rmul (m + k) = (n \rmul m) + (n \rmul k)$.
+%\end{proposition}
+%\begin{proof}
+%    Let $P = \{n \in \naturals \mid \forall m,k \in \naturals .  n \rmul (m + k) = (n \rmul m) + (n \rmul k)\}$.
+%    $\zero \in P$.
+%    $P \subseteq \naturals$.
+%    It suffices to show that for all $n \in P$ we have $\suc{n} \in P$.
+%    Fix $n \in P$.
+%    It suffices to show that for all $m'$ such that $m' \in \naturals$ we have for all $k' \in \naturals$ we have $\suc{n} \rmul (m' + k') = (\suc{n} \rmul m') + (\suc{n} \rmul k')$.
+%    Fix $m' \in \naturals$.
+%    Fix $k' \in \naturals$.
+%    $n \in \naturals$.
+%    $ \suc{n} \rmul (m' + k') = (n \rmul (m' + k')) + (m' + k') = ((n \rmul m') + (n \rmul k')) + (m' + k')  = ((n \rmul m') + (n \rmul k')) + m' + k'    = (((n \rmul m') + (n \rmul k')) + m') + k'  = (m' + ((n \rmul m') + (n \rmul k'))) + k'  = ((m' + (n \rmul m')) + (n \rmul k')) + k'  = (((n \rmul m') + m') + (n \rmul k')) + k'  = ((n \rmul m') + m') + ((n \rmul k') + k')  = (\suc{n} \rmul m') + (\suc{n} \rmul k')$.
+%\end{proof}
+
+\begin{proposition}\label{natural_disstro}
+    Suppose $n,m,k \in \naturals$.
+    Then $n \rmul (m + k) = (n \rmul m) + (n \rmul k)$.
+\end{proposition}
+\begin{proof}
+   %Let $P = \{n \in \naturals \mid \forall m,k \in \naturals . n \rmul (m + k) = (n \rmul m) + (n \rmul k)\}$.
+    Let $P = \{n \in \naturals \mid \text{for all $m,k \in \naturals$ we have $n \rmul (m + k) = (n \rmul m) + (n \rmul k)$}\}$.
+
+    $\zero \in P$.
+    $P \subseteq \naturals$.
+    It suffices to show that for all $n \in P$ we have $\suc{n} \in P$.
+    Fix $n \in P$.
+
+    It suffices to show that for all $m'$ such that $m' \in \naturals$ we have for all $k' \in \naturals$ we have $\suc{n} \rmul (m' + k') = (\suc{n} \rmul m') + (\suc{n} \rmul k')$.
+    Fix $m' \in \naturals$.
+    Fix $k' \in \naturals$.
+    $n \in \naturals$.
+    \begin{align*}
+        \suc{n} \rmul (m' + k') \\
+        &= (n \rmul (m' + k')) + (m' + k') \\% \explanation{by \cref{naturals_mul_axiom_2}}\\
+        &= ((n \rmul m') + (n \rmul k')) + (m' + k') \\%\explanation{by assumption}\\
+        &= ((n \rmul m') + (n \rmul k')) + m' + k'   \\%\explanation{by \cref{naturals_add_remove_brakets,naturals_add_kommu}}\\
+        &= (((n \rmul m') + (n \rmul k')) + m') + k' \\%\explanation{by \cref{naturals_add_kommu,naturals_add_remove_brakets,naturals_add_assoc}}\\
+        &= (m' + ((n \rmul m') + (n \rmul k'))) + k' \\%\explanation{by \cref{naturals_add_kommu}}\\
+        &= ((m' + (n \rmul m')) + (n \rmul k')) + k' \\%\explanation{by \cref{naturals_add_assoc}}\\
+        &= (((n \rmul m') + m') + (n \rmul k')) + k' \\%\explanation{by \cref{naturals_add_kommu}}\\
+        &= ((n \rmul m') + m') + ((n \rmul k') + k') \\%\explanation{by \cref{naturals_add_assoc}}\\
+        &= (\suc{n} \rmul m') + (\suc{n} \rmul k')   %\explanation{by \cref{naturals_mul_axiom_2}}
+    \end{align*}
+\end{proof}
+
+\begin{proposition}\label{naturals_rmul_one_kommu}
+    For all $n \in \naturals$ we have $n \rmul 1 = n$.
+\end{proposition}
+\begin{proof}
+    Let $P = \{ n \in \naturals \mid n \rmul 1 = n\}$.
+    $1 \in P$.
+    It suffices to show that for all $n' \in P$ we have $\suc{n'} \in P$.
+    Fix $n' \in P$.
+    It suffices to show that $\suc{n'} \rmul 1 = \suc{n'}$.
+    \begin{align*}
+        \suc{n'} \rmul 1 \\
+        &=  n' \rmul 1 + 1 \\
+        &=  n' + 1 \\
+        &= \suc{n'}
+    \end{align*}
+\end{proof}
+
+\begin{proposition}\label{naturals_rmul_kommu}
+    Let $n, m \in \naturals$.
+    Then $n \rmul m = m \rmul n$.
+\end{proposition}
+\begin{proof}
+    Let $P = \{n \in \naturals \mid \forall m \in \naturals. n \rmul m = m \rmul n\}$.
+    $\zero \in P$.
+    $P \subseteq \naturals$.
+    It suffices to show that for all $n \in P$ we have $\suc{n} \in P$.
+    Fix $n \in P$.
+    It suffices to show that for all $m \in \naturals$ we have $\suc{n} \rmul m = m \rmul \suc{n}$.
+    Fix $m \in \naturals$.
+    $n \rmul m = m \rmul n$.
+    \begin{align*}
+        \suc{n} \rmul m \\
+        &= (n \rmul m) + m \\
+        &= (m \rmul n) + m \\
+        &= m + (m \rmul n) \\
+        &= (m \rmul 1) + (m \rmul n) \\
+        &= m \rmul (1 + n) \\
+        &= m \rmul \suc{n} \\
+    \end{align*}
+\end{proof}
+
+\begin{proposition}\label{naturals_rmul_assoc}
+    Suppose $n,m,k \in \naturals$.
+    Then $n \rmul (m \rmul k) = (n \rmul m) \rmul k$.
+\end{proposition}
+\begin{proof}
+    Let $P = \{ n \in \naturals \mid \text{for all $m,k \in \naturals$ we have $n \rmul (m \rmul k) = (n \rmul m) \rmul k$ }\}$.
+    $\zero \in P$.
+    It suffices to show that for all $n' \in P$ we have $ \suc{n'} \in P$.
+    Fix $n' \in P$.
+    It suffices to show that for all $m' \in \naturals$ we have for all $k' \in \naturals$ we have $\suc{n'} \rmul (m' \rmul k') = (\suc{n'} \rmul m') \rmul k'$.
+    Fix $m' \in \naturals$.
+    Fix $k' \in \naturals$.
+    \begin{align*}
+        \suc{n'} \rmul (m' \rmul k')                \\
+        &=(n' \rmul (m' \rmul k')) + (m' \rmul k')  \\
+        &=((n' \rmul m') \rmul k') + (m' \rmul k')  \\
+        &=(k' \rmul (n' \rmul m')) + (k' \rmul m')  \\
+        &=k' \rmul ((n' \rmul m') + m')             \\
+        &=k' \rmul (\suc{n'} \rmul m')              \\
+        &=(\suc{n'} \rmul m') \rmul k'              
+    \end{align*}
+\end{proof}
+
+\begin{lemma}\label{naturals_is_equal_to_two_times_naturals}
+    $\{x+y \mid x \in \naturals, y \in \naturals \} = \naturals$.
+\end{lemma}
+
+
+\subsection{Axioms of the reals Part One}
+We seen before that we can proof the common behavior of the naturals.
+Since we now want to get furhter in a more efficient way, we introduce the basis axioms of the reals.
+Such that we can introduce the integers and raitionals as smooth as possible.
+
+
+
+The operations Multiplication and addition is closed in the reals
+\begin{axiom}\label{reals_rmul}
+    For all $n,m \in \reals$ we have $(n \rmul m) \in \reals$.
+\end{axiom}
+
+\begin{axiom}\label{reals_add}
+    For all $n,m \in \reals$ we have $(n + m) \in \reals$.
+\end{axiom}
+
+
+
+
+Commutivatiy of the standart operations
 \begin{axiom}\label{reals_axiom_kommu}
     For all $x,y \in \reals$ $x + y = y + x$ and $x \rmul y = y \rmul x$.
 \end{axiom}
   
+\begin{axiom}\label{reals_axiom_assoc}
+    For all $x,y,z \in \reals$ we have $(x + y) + z = x + (y + z)$.
+\end{axiom}
+
+
+Existence of  one and Zero
 \begin{axiom}\label{reals_axiom_zero}
     For all $x \in \reals$ $x + \zero = x$. 
 \end{axiom}
@@ -74,6 +400,9 @@
     For all $x \in \reals$ we have $x \rmul 1 = x$.
 \end{axiom}
 
+
+
+The Existence of Inverse of both operations
 \begin{axiom}\label{reals_axiom_add_invers}
     For all $x \in \reals$ there exist $y \in \reals$ such that $x + y = \zero$.
 \end{axiom}
@@ -82,49 +411,229 @@
     For all $x \in \reals$ such that $x \neq \zero$ there exist $y \in \reals$ such that $x \rmul y = 1$.
 \end{axiom}
 
+
+
+Disstrubitiv Laws of the reals
 \begin{axiom}\label{reals_axiom_disstro1}
     For all $x,y,z \in \reals$ $x \rmul (y + z) = (x \rmul y) + (x \rmul z)$.
 \end{axiom}
 
-\begin{axiom}\label{reals_axiom_dedekind_complete}
+\begin{axiom}\label{reals_disstro2}
+    For all $x,y,z \in \reals$ $(y + z) \rmul x = (y \rmul x) + (z \rmul x)$.
+\end{axiom}
+
+
+
+Definition of the order symbols
+\begin{abbreviation}\label{rless}
+    $x < y$ iff $x \rless y$.
+\end{abbreviation}
+
+\begin{abbreviation}\label{less_on_reals}
+    $x \leq y$ iff $x < y \lor x = y$.
+\end{abbreviation}
+
+\begin{abbreviation}\label{greater_on_reals}
+    $x > y$ iff $y < x$.
+\end{abbreviation}
+
+\begin{abbreviation}\label{greatereq_on_reals}
+    $x \geq y$ iff $y \leq x$.
+\end{abbreviation}
+
+
+
+Laws of the order on the reals
+\begin{abbreviation}\label{is_positiv}
+    $x$ is positiv iff $x > \zero$.
+\end{abbreviation}
+
+\begin{axiom}\label{reals_order}
+    For all $x,y \in \reals$ we have if $x < y$ then $\lnot y < x$.
+\end{axiom}
+
+\begin{axiom}\label{reals_dense}
+    For all $x,y \in \reals$ if $x < y$ then 
+    there exist $z \in \reals$ such that $x < z$ and $z < y$.
+\end{axiom}
+
+\begin{axiom}\label{reals_is_eta_zero_set}
     For all $X,Y,x,y$ such that $X,Y \subseteq \reals$ and $x \in X$ and $y \in Y$ and $x < y$ we have there exist $z \in \reals$
     such that $x < z < y$.
 \end{axiom}
 
-\begin{proposition}\label{reals_disstro2}
-    For all $x,y,z \in \reals$ $(y + z) \rmul x = (y \rmul x) + (z \rmul x)$.
+\begin{axiom}\label{reals_one_bigger_zero}
+    $\zero < 1$.
+\end{axiom}
+
+\begin{axiom}\label{reals_order_behavior_with_addition}
+    For all $x,y \in \reals$ such that $x < y$ we have for all $z \in \reals$ $x + z < y + z$.
+\end{axiom}
+
+\begin{axiom}\label{reals_postiv_mul_is_positiv}
+    For all $x,y \in \reals$ such that $\zero < x,y$ we have $\zero < (x \rmul y)$. 
+\end{axiom}
+
+\begin{axiom}\label{reals_postiv_mul_negativ_is_negativ}
+    For all $x,y \in \reals$ such that $x < \zero < y$ we have $(x \rmul y) < \zero$. 
+\end{axiom}
+
+\begin{axiom}\label{reals_negativ_mul_is_negativ}
+    For all $x,y \in \reals$ such that $x,y < \zero$ we have $\zero < (x \rmul y)$. 
+\end{axiom}
+
+
+
+
+\subsection{The Intergers}
+
+
+\begin{axiom}\label{neg}
+    For all $n \in \reals$ we have $\neg{n} \in \reals$ and $n + \neg{n} = \zero$.
+\end{axiom}
+
+\begin{axiom}\label{neg_of_zero}
+    $\neg{\zero} = \zero$.
+\end{axiom}
+
+\begin{definition}\label{minus}
+    $n - m = n + \neg{m}$.
+\end{definition}
+
+\begin{lemma}\label{minus_in_reals}
+    Suppose $n,m \in \reals$.
+    Then $n - m \in \reals$.
+\end{lemma}
+\begin{proof}
+    \begin{byCase}
+        \caseOf{$m = \zero$.} Trivial.
+        \caseOf{$m \neq \zero$.} Trivial.
+    \end{byCase}
+\end{proof}
+
+\begin{proposition}\label{negation_of_negation_is_id}
+    For all $r \in \reals$ we have $\neg{\neg{r}} = r$.
 \end{proposition}
 \begin{proof}
     Omitted.
+%    Fix $r \in \reals$.
+%    $r + \neg{r} = \zero$.
+%    $\neg{r} + \neg{\neg{r}} = \zero$.
+%    Follows by \cref{neg,reals_axiom_kommu}.
 \end{proof}
 
-\begin{proposition}\label{reals_reducion_on_addition}
-    For all $x,y,z \in \reals$ if $x + y = x + z$ then $y = z$.
-\end{proposition}
+\begin{definition}\label{integers}
+    $\integers = \{ z \in \reals \mid \exists n \in \naturals. z \in \naturals \lor  n + z = \zero\}$.
+\end{definition}
 
+\begin{lemma}\label{n_subset_z}
+    $\naturals \subseteq \integers$.
+\end{lemma}
 
+\begin{lemma}\label{neg_of_naturals_in_integers}
+    For all $n \in \naturals$ we have $\neg{n} \in \integers$.
+\end{lemma}
 
-%\begin{signature}\label{invers_is_set}
-%    $\addInv{y}$ is a set.
-%\end{signature}
+\begin{lemma}\label{integers_eq_naturals_and_negativ_naturals}
+    $\integers = \{ z \in \reals \mid \exists n \in \naturals. n = z \lor \neg{n} = z\}$.
+\end{lemma}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+\begin{abbreviation}\label{positiv_real_number}
+    $r$ is a positiv real number iff $r > \zero$ and $r \in \reals$.
+\end{abbreviation}
 
-%\begin{definition}\label{add_inverse}
-%    $\addInv{y} = \{ x \mid \exists k \in \reals. k + y = \zero \land x \in k\}$.
-%\end{definition}
-    
 
-%\begin{definition}\label{add_inverse_natural_language}
-%    $x$ is additiv inverse of $y$ iff $x = \addInv{y}$. 
-%\end{definition}
 
-%\begin{lemma}\label{rminus}
-%    $x \rminus \addInv{x} = \zero$.
-%\end{lemma}
+\subsection{The Rationals}
 
-\begin{abbreviation}\label{is_positiv}
-    $x$ is positiv iff $x > \zero$.
+\begin{axiom}\label{invers_reals}
+    For all $q \in \reals$ we have $\inv{q} \rmul q = 1$.
+\end{axiom}
+
+\begin{abbreviation}\label{rfrac}
+    $\rfrac{x}{y} = x \rmul \inv{y}$.
+\end{abbreviation}
+
+\begin{abbreviation}\label{naturalsplus}
+    $\naturalsPlus = \naturals \setminus \{\zero\}$.
+\end{abbreviation}
+
+\begin{definition}\label{rationals} %TODO: Vielleicht ist hier die definition das alle inversen von den ganzenzahlen und die ganzenzahlen selbst die rationalen zahlen erzeugen
+    $\rationals = \{ q \in \reals \mid \exists z \in \integers. \exists n \in (\integers \setminus \{\zero\}). q = \rfrac{z}{n} \}$.
+\end{definition}
+
+\begin{abbreviation}\label{nominator}
+    $z$ is nominator of $q$ iff there exists $n \in \naturalsPlus$ such that $q = \rfrac{z}{n}$.
+\end{abbreviation}
+
+\begin{abbreviation}\label{denominator}
+    $n$ is denominator of $q$ iff there exists $z \in \integers$ such that $q = \rfrac{z}{n}$.
 \end{abbreviation}
 
+\begin{theorem}\label{one_divided_by_n_is_in_zero_to_one}
+    For all $n \in \naturalsPlus$ we have $\zero < \rfrac{1}{n} \leq 1$.
+\end{theorem}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+\begin{lemma}\label{fraction_kuerzung} %TODO: Englischen namen rausfinden
+    For all $n,m,k \in \reals$ we have $\rfrac{n \rmul k}{m \rmul k} = \rfrac{n}{m}$.
+\end{lemma}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+\begin{lemma}\label{fraction_swap}
+    For all $n,m,k,l \in \reals$ we have $\rfrac{\rfrac{n}{m}}{\rfrac{k}{l}}=\rfrac{n \rmul l}{m \rmul k}$.
+\end{lemma}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+\begin{definition}\label{divisor}
+    $g$ is a integral divisor of $a$ iff $g \in \naturals$ and there exist $b \in \integers$ such that $g \rmul b = a$.
+\end{definition}
+
+
+
+
+%\begin{abbreviation}\label{gcd}
+%    $g$ is greatest common divisor of $\{a,b\}$ iff
+%    $g$ is a integral divisor of $a$ 
+%    and $g$ is a integral divisor of $b$ 
+%    and for all $g'$ such that $g'$ is a integral divisor of $a$
+%    and $g'$ is a integral divisor of $b$ we have $g' \leq g$.
+%\end{abbreviation}
+% TODO:  Was man noch so beweisen könnte: bruch kürzung, kehrbruch eigenschaften, bruch in bruch vereinfachung, 
+
+
+\subsection{Order on the reals}
+
+\begin{axiom}\label{reals_order_is_transitive}
+    For all $x,y,z \in \reals$ such that $x < y$ and $y < z$ we have $x < z$.
+\end{axiom}
+
+
+\begin{lemma}\label{plus_one_order}
+    For all $r\in \reals$ we have $ r < r + 1$.
+\end{lemma}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+\begin{lemma}\label{negation_and_order}
+    Suppose $r \in \reals$.
+    $r \leq \zero$ iff $\zero \leq \neg{r}$.
+\end{lemma}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+
 \begin{lemma}\label{reals_add_of_positiv}
     Let $x,y \in \reals$.
     Suppose $x$ is positiv and $y$ is positiv.
@@ -184,7 +693,7 @@
 
 \begin{lemma}\label{order_reals_lemma3}
     Let $x,y,z \in \reals$.
-    Suppose $\zero < x$. 
+    Suppose $\zero > x$. 
     Suppose $y < z$. 
     Then $(x \rmul z) < (x \rmul y)$.
 \end{lemma}
@@ -195,7 +704,9 @@
 \begin{lemma}\label{order_reals_lemma00}
     For all $x,y \in \reals$ such that $x > y$ we have $x \geq y$.
 \end{lemma}
-
+\begin{proof}
+    Omitted.
+\end{proof}
 
 \begin{lemma}\label{order_reals_lemma5}
     For all $x,y \in \reals$ such that $x < y$ we have $x \leq y$.
@@ -212,7 +723,7 @@
 \end{proof}
 
 \begin{lemma}\label{reals_minus}
-    Assume $x,y \in \reals$. If $x \rminus y = \zero$ then $x=y$.
+    Assume $x,y \in \reals$. If $x - y = \zero$ then $x=y$.
 \end{lemma}
 \begin{proof}
     Omitted.
@@ -260,34 +771,73 @@
     $x$ is the supremum of $X$ iff $x$ is a greatest lower bound of $X$.
 \end{definition}
 
+\begin{definition}\label{minimum}
+    $\min{X} = \{x \in X \mid \forall y \in X. x \leq y \}$.
+\end{definition}
+
+
+\begin{definition}\label{maximum}
+    $\max{X} = \{x \in X \mid \forall y \in X. x \geq y \}$.
+\end{definition}
+
+
+\begin{definition}\label{intervalclosed}
+    $\intervalclosed{a}{b} = \{x \in \reals \mid a \leq x \leq b\}$.
+\end{definition}
+
+
+\begin{definition}\label{intervalopen}
+    $\intervalopen{a}{b} = \{ x \in \reals \mid a < x < b\}$.
+\end{definition}
+
+\begin{definition}\label{intervalopen_infinite_left}
+    $\intervalopenInfiniteLeft{b} = \{ x \in \reals \mid x < b\}$.
+\end{definition}
+
+\begin{definition}\label{intervalopen_infinite_right}
+    $\intervalopenInfiniteRight{a} = \{ x \in \reals \mid x > a\}$.
+\end{definition}
+
+\begin{definition}\label{intervalclosed_infinite_left}
+    $\intervalclosedInfiniteLeft{b} = \{ x \in \reals \mid x \leq b\}$.
+\end{definition}
+
+\begin{definition}\label{intervalclosed_infinite_right}
+    $\intervalclosedInfiniteRight{a} = \{ x \in \reals \mid x \geq a\}$.
+\end{definition}
+
+
+\begin{definition}\label{m_to_n_set}
+    $\seq{m}{n} = \{x \in \naturals \mid  m \leq x \leq n\}$.   
+\end{definition}
+
+\begin{axiom}\label{abs_behavior1}
+    If $x \geq \zero$ then $\abs{x} = x$.
+\end{axiom}
+
+\begin{axiom}\label{abs_behavior2}
+    If $x < \zero$ then $\abs{x} = \neg{x}$.
+\end{axiom}
+
+\begin{definition}\label{realsminus}
+    $\realsminus = \{r \in \reals \mid r < \zero\}$.
+\end{definition}
+
+\begin{definition}\label{realsplus}
+    $\realsplus = \{r \in \reals \mid r > \zero\}$.
+\end{definition}
+
+\begin{definition}\label{epsilon_ball}
+    $\epsBall{x}{\epsilon} = \intervalopen{x-\epsilon}{x+\epsilon}$.
+\end{definition}
 
 
 
-\section{The natural numbers}
 
 
-\begin{abbreviation}\label{def_suc}
-    $\successor{n} = n + 1$.
-\end{abbreviation}
 
-\begin{inductive}\label{naturals_definition_as_subset_of_reals}
-    Define $\nat \subseteq \reals$ inductively as follows.
-    \begin{enumerate}
-        \item $\zero \in \nat$.
-        \item If $n\in \nat$, then $\successor{n} \in \nat$. 
-    \end{enumerate}
-\end{inductive}
 
-\begin{lemma}\label{reals_order_suc}
-    $n < \successor{n}$.
-\end{lemma}
 
 %\begin{proposition}\label{safe}
 %    Contradiction.
 %\end{proposition}
-
-\section{The integers}
-
-%\begin{definition}
-%    $\integers = \{z \in \reals \mid z = \zero or \} $.
-%\end{definition}
\ No newline at end of file
diff --git a/library/ordinal.tex b/library/ordinal.tex
index 3063162..6f924c1 100644
--- a/library/ordinal.tex
+++ b/library/ordinal.tex
@@ -3,7 +3,7 @@
 \import{set/powerset.tex}
 \import{set/regularity.tex}
 \import{set/suc.tex}
-\import{nat.tex}
+%\import{nat.tex}
 
 
 \section{Transitive sets}
@@ -584,55 +584,56 @@ Then $\alpha\subseteq\beta$.
     Follows by \cref{subseteq_antisymmetric}.
 \end{proof}
 
-
-\subsection{Natural numbers as ordinals}
-
-\begin{lemma}\label{nat_is_successor_ordinal}
-    Let $n\in\naturals$.
-    Suppose $n\neq \emptyset$.
-    Then $n$ is a successor ordinal.
-\end{lemma}
-\begin{proof}
-    Let $M = \{ m\in \naturals \mid\text{$m = \emptyset$ or $m$ is a successor ordinal}\}$.
-    $M$ is an inductive set by \cref{suc_ordinal,naturals_inductive_set,successor_ordinal,emptyset_is_ordinal}.
-    Now $M\subseteq \naturals\subseteq M$
-        by \cref{subseteq,naturals_smallest_inductive_set}.
-    Thus $M = \naturals$.
-    Follows by \cref{subseteq}.
-\end{proof}
-
-\begin{lemma}\label{nat_is_transitiveset}
-    $\naturals$ is \in-transitive.
-\end{lemma}
-\begin{proof}
-    Let $M = \{ m\in\naturals \mid \text{for all $n\in m$ we have $n\in\naturals$} \}$.
-    $\emptyset\in M$.
-    For all $n\in M$ we have $\suc{n}\in M$
-        by \cref{naturals_inductive_set,suc}.
-    Thus $M$ is an inductive set.
-    Now $M\subseteq \naturals\subseteq M$
-        by \cref{subseteq,naturals_smallest_inductive_set}.
-    Hence $\naturals = M$.
-\end{proof}
-
-\begin{lemma}\label{natural_number_is_ordinal}
-    Every natural number is an ordinal.
-\end{lemma}
-\begin{proof}
-    Follows by \cref{suc_ordinal,suc_neq_emptyset,naturals_inductive_set,nat_is_successor_ordinal,successor_ordinal,suc_ordinal_implies_ordinal}.
-\end{proof}
-
-\begin{lemma}\label{omega_is_an_ordinal}
-    $\naturals$ is an ordinal.
-\end{lemma}
-\begin{proof}
-    Follows by \cref{natural_number_is_ordinal,transitive_set_of_ordinals_is_ordinal,nat_is_transitiveset}.
-\end{proof}
-
-\begin{lemma}\label{omega_is_a_limit_ordinal}
-    $\naturals$ is a limit ordinal.
-\end{lemma}
-\begin{proof}
-    $\emptyset\precedes \naturals$.
-    If $n\in \naturals$, then $\suc{n}\in\naturals$.
-\end{proof}
+%
+%\subsection{Natural numbers as ordinals}
+%
+%\begin{lemma}\label{nat_is_successor_ordinal}
+%    Let $n\in\naturals$.
+%    Suppose $n\neq \emptyset$.
+%    Then $n$ is a successor ordinal.
+%\end{lemma}
+%\begin{proof}
+%    Let $M = \{ m\in \naturals \mid\text{$m = \emptyset$ or $m$ is a successor ordinal}\}$.
+%    $M$ is an inductive set by \cref{suc_ordinal,naturals_inductive_set,successor_ordinal,emptyset_is_ordinal}.
+%    Now $M\subseteq \naturals\subseteq M$
+%        by \cref{subseteq,naturals_smallest_inductive_set}.
+%    Thus $M = \naturals$.
+%    Follows by \cref{subseteq}.
+%\end{proof}
+%
+%\begin{lemma}\label{nat_is_transitiveset}
+%    $\naturals$ is \in-transitive.
+%\end{lemma}
+%\begin{proof}
+%    Let $M = \{ m\in\naturals \mid \text{for all $n\in m$ we have $n\in\naturals$} \}$.
+%    $\emptyset\in M$.
+%    For all $n\in M$ we have $\suc{n}\in M$
+%        by \cref{naturals_inductive_set,suc}.
+%    Thus $M$ is an inductive set.
+%    Now $M\subseteq \naturals\subseteq M$
+%        by \cref{subseteq,naturals_smallest_inductive_set}.
+%    Hence $\naturals = M$.
+%\end{proof}
+%
+%\begin{lemma}\label{natural_number_is_ordinal}
+%    Every natural number is an ordinal.
+%\end{lemma}
+%\begin{proof}
+%    Follows by \cref{suc_ordinal,suc_neq_emptyset,naturals_inductive_set,nat_is_successor_ordinal,successor_ordinal,suc_ordinal_implies_ordinal}.
+%\end{proof}
+%
+%\begin{lemma}\label{omega_is_an_ordinal}
+%    $\naturals$ is an ordinal.
+%\end{lemma}
+%\begin{proof}
+%    Follows by \cref{natural_number_is_ordinal,transitive_set_of_ordinals_is_ordinal,nat_is_transitiveset}.
+%\end{proof}
+%
+%\begin{lemma}\label{omega_is_a_limit_ordinal}
+%    $\naturals$ is a limit ordinal.
+%\end{lemma}
+%\begin{proof}
+%    $\emptyset\precedes \naturals$.
+%    If $n\in \naturals$, then $\suc{n}\in\naturals$.
+%\end{proof}
+%
\ No newline at end of file
diff --git a/library/relation.tex b/library/relation.tex
index 4c4065f..d63e747 100644
--- a/library/relation.tex
+++ b/library/relation.tex
@@ -633,6 +633,7 @@ This lets us use the same symbol for composition of functions.
 \begin{proof}
     %$x\in\dom{R}$ and $z\in\ran{S}$.
     There exists $y$ such that $x\mathrel{R} y\mathrel{S} z$ by \cref{circ,pair_eq_iff}.
+    Follows by assumption.
 \end{proof}
 
 \begin{proposition}\label{circ_iff}
diff --git a/library/relation/equivalence.tex b/library/relation/equivalence.tex
index 87f70af..0c5dbfa 100644
--- a/library/relation/equivalence.tex
+++ b/library/relation/equivalence.tex
@@ -219,54 +219,59 @@
 \end{proof}
 
 
-%
-%\begin{definition}\label{equivalence_from_partition}
-%    $\equivfrompartition{P} = \{(a, b)\mid a\in A, b\in A\mid \exists C\in P.\ a, b\in C\}$.
-%\end{definition}
-%
-%\begin{proposition}\label{equivalence_from_partition_intro}
-%    Let $P$ be a partition of $A$.
-%    Let $a,b\in A$.
-%    Suppose $a,b\in C\in P$.
-%    Then $a\mathrel{\equivfrompartition{P}} b$.
-%\end{proposition}
-%
-%\begin{proposition}\label{equivalence_from_partition_reflexive}
-%    Let $P$ be a partition of $A$.
-%    $\equivfrompartition{P}$ is reflexive on $A$.
-%\end{proposition}
-%
-%\begin{proposition}\label{equivalence_from_partition_symmetric}
-%    Let $P$ be a partition.
-%    $\equivfrompartition{P}$ is symmetric.
-%\end{proposition}
-%\begin{proof}
-%    Follows by \cref{symmetric,equivalence_from_partition,notin_emptyset}.
-%\end{proof}
-%
-%\begin{proposition}\label{equivalence_from_partition_transitive}
-%    Let $P$ be a partition.
-%    $\equivfrompartition{P}$ is transitive.
-%\end{proposition}
-%
-%\begin{proposition}\label{equivalence_from_partition_is_equivalence}
-%    Let $P$ be a partition of $A$.
-%    $\equivfrompartition{P}$ is an equivalence on $A$.
-%\end{proposition}
-%
-%\begin{proposition}\label{equivalence_from_quotient}
-%    Let $E$ be an equivalence on $A$.
-%    Then $\equivfrompartition{\quotient{A}{E}} = E$.
-%\end{proposition}
-%\begin{proof}
-%    Follows by set extensionality.
-%\end{proof}
-%
-%\begin{proposition}\label{partition_eq_quotient_by_equivalence_from_partition}
-%    Let $P$ be a partition of $A$.
-%    Then $\quotient{A}{\equivfrompartition{P}} = P$.
-%\end{proposition}
-%\begin{proof}
-%    Follows by set extensionality.
-%\end{proof}
-%
\ No newline at end of file
+
+\begin{definition}\label{equivalence_from_partition}
+    $\equivfrompartition{P}{A} = \{(a, b)\mid a\in A, b\in A\mid \exists C\in P.\ a, b\in C\}$.
+\end{definition}
+
+\begin{proposition}\label{equivalence_from_partition_intro}
+    Let $P$ be a partition of $A$.
+    Let $a,b\in A$.
+    Suppose $a,b\in C\in P$.
+    Then $a\mathrel{\equivfrompartition{P}{A}} b$.
+\end{proposition}
+
+\begin{proposition}\label{equivalence_from_partition_reflexive}
+    Let $P$ be a partition of $A$.
+    $\equivfrompartition{P}{A}$ is reflexive on $A$.
+\end{proposition}
+
+\begin{proposition}\label{equivalence_from_partition_symmetric}
+    Let $P$ be a partition.
+    $\equivfrompartition{P}{A}$ is symmetric.
+\end{proposition}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+\begin{proposition}\label{equivalence_from_partition_transitive}
+    Let $P$ be a partition.
+    $\equivfrompartition{P}{A}$ is transitive.
+\end{proposition}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+\begin{proposition}\label{equivalence_from_partition_is_equivalence}
+    Let $P$ be a partition of $A$.
+    $\equivfrompartition{P}{A}$ is an equivalence on $A$.
+\end{proposition}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+\begin{proposition}\label{equivalence_from_quotient}
+    Let $E$ be an equivalence on $A$.
+    Then $\equivfrompartition{\quotient{A}{E}}{A} = E$.
+\end{proposition}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+\begin{proposition}\label{partition_eq_quotient_by_equivalence_from_partition}
+    Let $P$ be a partition of $A$.
+    Then $\quotient{A}{\equivfrompartition{P}{A}} = P$.
+\end{proposition}
+\begin{proof}
+    Omitted.
+\end{proof}
diff --git a/library/set/equinumerosity.tex b/library/set/equinumerosity.tex
index a846b78..a922052 100644
--- a/library/set/equinumerosity.tex
+++ b/library/set/equinumerosity.tex
@@ -15,7 +15,7 @@
     $A\approx A$.
 \end{proposition}
 \begin{proof}
-    $\identity{A}$ is a bijection from $A$ to $A$ by \cref{id_is_bijection}.
+    $\identity{A}$ is a bijection from $A$ to $A$. %by \cref{id_is_bijection}.
     Follows by \cref{equinum}.
 \end{proof}
 
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 6a32353..95c4d0a 100644
--- a/library/topology/continuous.tex
+++ b/library/topology/continuous.tex
@@ -1,5 +1,9 @@
 \import{topology/topological-space.tex}
 \import{relation.tex}
+\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]$.
@@ -8,18 +12,25 @@
 \begin{proposition}\label{continuous_definition_by_closeds}
     Let $X$ be a topological space.
     Let $Y$ be a topological space.
+    Let $f \in \funs{X}{Y}$.
     Then $f$ is continuous iff for all $U \in \closeds{Y}$ we have $\preimg{f}{U} \in \closeds{X}$.
 \end{proposition}
 \begin{proof}
     Omitted.
-    %We show that if $f$ is continuous then for all $U \in \closeds{Y}$ we have $\preimg{f}{U} \in \closeds{X}$.
+    %We show that if $f$ is continuous then for all $U \in \closeds{Y}$ such that $U \neq \emptyset$ we have $\preimg{f}{U} \in \closeds{X}$.
     %\begin{subproof}
     %    Suppose $f$ is continuous.
     %    Fix $U \in \closeds{Y}$.
     %    $\carrier[Y] \setminus U$ is open in $Y$.
     %    Then $\preimg{f}{(\carrier[Y] \setminus U)}$ is open in $X$.
     %    Therefore $\carrier[X] \setminus \preimg{f}{(\carrier[Y] \setminus U)}$ is closed in $X$.
-    %    $\carrier[X] \setminus \preimg{f}{(\carrier[Y] \setminus U)} \subseteq \preimg{f}{U}$.
+    %    We show that $\carrier[X] \setminus \preimg{f}{(\carrier[Y] \setminus U)} \subseteq \preimg{f}{U}$.
+    %    \begin{subproof}
+    %        It suffices to show that for all $x \in \carrier[X] \setminus \preimg{f}{(\carrier[Y] \setminus U)}$ we have $x \in \preimg{f}{U}$.
+    %        Fix $x \in \carrier[X] \setminus \preimg{f}{(\carrier[Y] \setminus U)}$.
+    %        Take $y \in \carrier[Y]$ such that $f(x)=y$.
+    %        It suffices to show that $y \in U$.
+    %    \end{subproof}
     %    $\preimg{f}{U} \subseteq \carrier[X] \setminus \preimg{f}{(\carrier[Y] \setminus U)}$.
     %\end{subproof}
     %We show that if for all $U \in \closeds{Y}$ we have $\preimg{f}{U} \in \closeds{X}$ then $f$ is continuous.
@@ -27,3 +38,4 @@
     %    Omitted.
     %\end{subproof}
 \end{proof}
+
diff --git a/library/topology/metric-space.tex b/library/topology/metric-space.tex
index bcc5b8c..031aa0f 100644
--- a/library/topology/metric-space.tex
+++ b/library/topology/metric-space.tex
@@ -4,7 +4,7 @@
 \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 $\reals$ and
diff --git a/library/topology/real-topological-space.tex b/library/topology/real-topological-space.tex
new file mode 100644
index 0000000..db7ee94
--- /dev/null
+++ b/library/topology/real-topological-space.tex
@@ -0,0 +1,786 @@
+\import{set.tex}
+\import{set/cons.tex}
+\import{set/powerset.tex}
+\import{set/fixpoint.tex}
+\import{set/product.tex}
+\import{topology/topological-space.tex}
+\import{topology/separation.tex}
+\import{topology/continuous.tex}
+\import{topology/basis.tex}
+\import{numbers.tex}
+\import{function.tex}
+
+
+\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\}$.
+\end{definition}
+
+\begin{axiom}\label{reals_carrier_reals}
+    $\carrier[\reals] = \reals$.
+\end{axiom}
+
+\begin{lemma}\label{intervals_are_connected_in_reals}
+    Suppose $a,b \in \reals$.
+    Then for all $c \in \reals$ such that $a < c < b$ we have $c \in \intervalopen{a}{b}$.
+\end{lemma}
+
+\begin{lemma}\label{epsball_are_subset_reals_elem}
+    Suppose $x \in \reals$.
+    Suppose $\epsilon \in \realsplus$.
+    Then for all $y \in \epsBall{x}{\epsilon}$ we have $y \in \reals$.
+\end{lemma}
+
+\begin{lemma}\label{intervalopen_iff}
+    Suppose $a,b,c \in \reals$.
+    Suppose $a < b$.
+    $c \in \intervalopen{a}{b}$ iff $a < c < b$.
+\end{lemma}
+
+\begin{lemma}\label{epsball_are_subseteq_reals_set}
+    Suppose $x \in \reals$.
+    Suppose $\epsilon \in \realsplus$.
+    Then $\epsBall{x}{\epsilon} \subseteq \reals$.
+\end{lemma}
+
+\begin{lemma}\label{epsball_are_subset_reals_set}
+    Suppose $x \in \reals$.
+    Suppose $\epsilon \in \realsplus$.
+    Then $\epsBall{x}{\epsilon} \subset \reals$.
+\end{lemma}
+
+\begin{lemma}\label{reals_order_minus_positiv}
+    Suppose $x,y \in \reals$.
+    Suppose $\zero < y$.
+    $x - y < x$.
+\end{lemma}
+
+\begin{lemma}\label{realsplus_bigger_zero}
+    For all $x \in \realsplus$ we have $\zero < x$.
+\end{lemma}
+
+\begin{lemma}\label{realsplus_in_reals}
+    For all $x \in \realsplus$ we have $x \in \reals$.
+\end{lemma}
+
+\begin{lemma}\label{epsball_are_inhabited}
+    Suppose $x \in \reals$.
+    Suppose $\epsilon \in \realsplus$.
+    Then $\epsBall{x}{\epsilon}$ is inhabited.
+\end{lemma}
+\begin{proof}
+    $x < x + \epsilon$ by \cref{reals_order_behavior_with_addition,realsplus,reals_axiom_zero_in_reals,reals_axiom_kommu,reals_axiom_zero}.
+    $x - \epsilon < x$.
+    $x \in \epsBall{x}{\epsilon}$.
+\end{proof}
+
+\begin{lemma}\label{reals_elem_inbetween}
+    For all $a,b \in \reals$ such that $a < b$ we have there exists $c \in \reals$ such that $a < c < b$.
+\end{lemma}
+
+\begin{lemma}\label{epsball_equal_openinterval}
+    Suppose $x \in \reals$.
+    Suppose $\epsilon \in \realsplus$.
+    Then $\epsBall{x}{\epsilon} = \intervalopen{x - \epsilon}{x + \epsilon}$.
+\end{lemma}
+
+\begin{lemma}\label{minus_behavior1}
+    For all $x \in \reals$ we have $x - x = \zero$.
+\end{lemma}
+
+\begin{lemma}\label{minus_behavior2}
+    For all $x \in \reals$ we have $x + \neg{x} = \zero$.
+\end{lemma}
+
+\begin{lemma}\label{minus_behavior3}
+    For all $x \in \reals$ we have $\neg{x} = \zero - x$.
+\end{lemma}
+
+\begin{lemma}\label{reals_order_is_addition_with_positiv_number}
+    For all $x,y \in \reals$ such that $x < y$ we have there exists $z \in \realsplus$ such that $x + z = y$.
+\end{lemma}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+
+
+
+\begin{lemma}\label{reals_order_plus_minus}
+    Suppose $a,b \in \reals$.
+    Suppose $\zero < b$.
+    Then $(a-b) < (a+b)$.
+\end{lemma}
+\begin{proof}
+    We show that $a < (a+b)$.
+    \begin{subproof}
+        Trivial.
+    \end{subproof}
+    We show that $(a-b) < a$.
+    \begin{subproof}
+        Trivial.
+    \end{subproof}
+\end{proof}
+
+\begin{lemma}\label{epsball_are_connected_in_reals}
+    Suppose $x \in \reals$.
+    Suppose $\epsilon \in \realsplus$.
+    Then for all $c \in \reals$ such that $(x - \epsilon) < c < (x + \epsilon)$ we have $c \in \epsBall{x}{\epsilon}$.
+\end{lemma}
+\begin{proof}
+    $x - \epsilon \in \reals$.
+    $x + \epsilon \in \reals$.
+
+
+    It suffices to show that for all $c$ such that $c \in \reals \land (x - \epsilon) \rless c \rless (x + \epsilon)$ we have $c \in \epsBall{x}{\epsilon}$.
+    Fix $c$ such that $(c \in \reals) \land (x - \epsilon) \rless c \rless (x + \epsilon)$.
+    $(x - \epsilon) < c < (x + \epsilon)$.
+\end{proof}
+
+\begin{theorem}\label{topological_basis_reals_is_prebasis}
+    $\topoBasisReals$ is a topological prebasis for $\reals$.
+\end{theorem}
+\begin{proof}
+    We show that $\unions{\topoBasisReals} \subseteq \reals$.
+    \begin{subproof}
+        It suffices to show that for all $x \in \unions{\topoBasisReals}$ we have $x \in \reals$.
+        Fix $x \in \unions{\topoBasisReals}$.
+        \begin{byCase}
+            \caseOf{$x = \emptyset$.}
+                Trivial.
+            \caseOf{$x \neq \emptyset$.}
+                %There exists $U \in \topoBasisReals$ such that $x \in U$.
+                Take $U \in \topoBasisReals$ such that $x \in U$.
+                Follows by \cref{epsball_are_subseteq_reals_set,topological_basis_reals_eps_ball,epsilon_ball,minus,subseteq}.
+        \end{byCase}
+    \end{subproof}
+    We show that $\reals \subseteq \unions{\topoBasisReals}$.
+    \begin{subproof}
+        It suffices to show that for all $x \in \reals$ we have $x \in \unions{\topoBasisReals}$.
+        Fix $x \in \reals$.
+        $\epsBall{x}{1} \in \topoBasisReals$.
+        Therefore $x \in \unions{\topoBasisReals}$ by \cref{one_in_reals,reals_one_bigger_zero,unions_intro,realsplus,plus_one_order,reals_order_minus_positiv,epsball_are_connected_in_reals}.
+    \end{subproof}
+\end{proof}
+
+%\begin{lemma}\label{intervl_intersection_is_interval}
+%    Suppose $a,b,a',b' \in \reals$.
+%    Suppose there exist $x \in \reals$ such that $x \in \intervalopen{a}{b} \inter \intervalopen{a'}{b'}$.
+%    Then there exists $q,p \in \reals$ such that $q < p$ and $\intervalopen{q}{p} \subseteq \intervalopen{a}{b} \inter \intervalopen{a'}{b'}$.
+%\end{lemma}
+%
+
+\begin{lemma}\label{reals_order_total}
+    For all $x,y \in \reals$ we have either $x < y$ or $x \geq y$. 
+\end{lemma}
+\begin{proof}
+    It suffices to show that for all $x \in \reals$ we have for all $y \in \reals$ we have either $x < y$ or $x \geq y$. 
+    Fix $x \in \reals$.
+    Fix $y \in \reals$.
+    Omitted.
+\end{proof}
+
+\begin{lemma}\label{topo_basis_reals_eps_iff}
+    $X \in \topoBasisReals$ iff there exists $x_0, \delta$ such that $x_0 \in \reals$ and $\delta \in \realsplus$ and $\epsBall{x_0}{\delta} = X$.
+\end{lemma}
+
+\begin{lemma}\label{topo_basis_reals_intro}
+For all $x,\delta$ such that $x \in \reals \land \delta \in \realsplus$ we have $\epsBall{x}{\delta} \in \topoBasisReals$.
+\end{lemma}
+
+\begin{lemma}\label{realsplus_in_reals_plus}
+    For all $x,y$ such that $x \in \reals$ and $y \in \realsplus$ we have $x + y \in \reals$.
+\end{lemma}
+
+\begin{lemma}\label{realspuls_in_reals_minus}
+    For all $x,y$ such that $x \in \reals$ and $y \in \realsplus$ we have $x - y \in \reals$.
+\end{lemma}
+
+\begin{lemma}\label{eps_ball_implies_open_interval}
+    Suppose $x \in \reals$.
+    Suppose $\epsilon \in \realsplus$. 
+    Then there exists $a,b \in \reals$ such that $a < b$ and $\intervalopen{a}{b} = \epsBall{x}{\epsilon}$.
+\end{lemma}
+
+\begin{lemma}\label{one_in_realsplus}
+    $1 \in \realsplus$.
+\end{lemma}
+
+\begin{lemma}\label{reals_existence_addition_reverse}
+    For all $\delta \in \reals$ there exists $\epsilon \in \reals$ such that $\epsilon + \epsilon = \delta$.
+\end{lemma}
+\begin{proof}
+    Fix $\delta \in \reals$.
+    Follows by \cref{one_in_realsplus,reals_disstro2,reals_axiom_disstro1,reals_rmul,suc_eq_plus_one,reals_axiom_mul_invers,suc,suc_neq_emptyset,realsplus_in_reals_plus,naturals_addition_axiom_2,naturals_1_kommu,reals_axiom_zero,naturals_inductive_set,one_is_suc_zero,realsplus,reals_one_bigger_zero,one_in_reals,reals_axiom_one,minus_in_reals}.
+\end{proof}
+
+\begin{lemma}\label{reals_addition_minus_behavior1}
+    For all $a,b,c \in \reals$ such that $a = b + c$ we have $b = a - c$.
+\end{lemma}
+\begin{proof}
+    It suffices to show that for all $a \in \reals$ for all $b \in \reals$ for all $c \in \reals$ if $a = b + c$ then $b = a - c$.
+    Fix $a \in \reals$.
+    Fix $b \in \reals$.
+    Fix $c \in \reals$.
+    Suppose $a = b + c$.
+    Then $a + \neg{c} = b + c + \neg{c}$.
+    Therefore $a - c = b + c + \neg{c}$.
+    $a - c = (b + c) - c$.
+    $(b + c) - c = (b + c) + \neg{c}$.
+    $(b + c) + \neg{c} = b + (c + \neg{c})$.
+    $b + (c + \neg{c}) = b + (\zero)$.
+    $a - c = b$.
+\end{proof}
+
+\begin{lemma}\label{reals_addition_minus_behavior2}
+    For all $a,b,c \in \reals$ such that $a = b - c$ we have $b = c + a$.
+\end{lemma}
+
+\begin{lemma}\label{open_interval_eq_eps_ball}
+    Suppose $a,b \in \reals$.
+    Suppose $a < b$.
+    Then there exist $x,\epsilon$ such that $x \in \reals$ and $\epsilon \in \realsplus$ and $\intervalopen{a}{b} = \epsBall{x}{\epsilon}$.
+\end{lemma}
+\begin{proof}
+    Let $\delta = (b-a)$.
+    $\delta$ is positiv by \cref{minus_in_reals,minus_behavior3,reals_axiom_zero_in_reals,reals_order_behavior_with_addition,minus_behavior1,minus}.
+    There exists $\epsilon \in \reals$ such that $\epsilon + \epsilon = \delta$.
+    Let $x = a + \epsilon$.
+    $a + \delta = b$.
+    $a + \epsilon + \epsilon = b$. 
+    $x + \epsilon = b$.
+    $\epsilon \in \realsplus$ by \cref{reals_order_behavior_with_addition,reals_axiom_kommu,reals_axiom_zero,reals_order_is_transitive,reals_add,minus_behavior1,minus_behavior3,minus,reals_order_total,reals_axiom_zero_in_reals,realsplus}.
+    $a = x - \epsilon$.
+    $b = x + \epsilon$.
+    We show that $\intervalopen{a}{b} \subseteq \epsBall{x}{\epsilon}$.
+    \begin{subproof}
+        It suffices to show that for all $y \in \intervalopen{a}{b}$ we have $y \in \epsBall{x}{\epsilon}$.
+        Fix $y \in \intervalopen{a}{b}$.
+    \end{subproof}
+    We show that $\epsBall{x}{\epsilon} \subseteq \intervalopen{a}{b}$.
+    \begin{subproof}
+        It suffices to show that for all $y \in \epsBall{x}{\epsilon}$ we have $y \in \intervalopen{a}{b}$ by \cref{subseteq}.
+        Fix $y \in \epsBall{x}{\epsilon}$.
+    \end{subproof}
+
+\end{proof}
+
+\begin{lemma}\label{intersection_openinterval_inclusion_of_border}
+    Suppose $a,b,x,y \in \reals$.
+    Suppose $a < b$.
+    Suppose $x < y$.
+    Suppose $a \leq x < y \leq b$.
+    Then $\intervalopen{a}{b} \inter \intervalopen{x}{y} = \intervalopen{x}{y}$.
+\end{lemma}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+\begin{lemma}\label{intersection_openinterval_lower_border_eq}
+    Suppose $a,b,x,y \in \reals$.
+    Suppose $a < b$.
+    Suppose $x < y$.
+    Suppose $a = x$ and $b \leq y$.
+    Then $\intervalopen{a}{b} \inter \intervalopen{x}{y} = \intervalopen{a}{b}$.
+\end{lemma}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+\begin{lemma}\label{intersection_openinterval_upper_border_eq}
+    Suppose $a,b,x,y \in \reals$.
+    Suppose $a < b$.
+    Suppose $x < y$.
+    Suppose $a \leq x$ and $b = y$.
+    Then $\intervalopen{a}{b} \inter \intervalopen{x}{y} = \intervalopen{x}{y}$.
+\end{lemma}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+\begin{lemma}\label{intersection_openinterval_none_border_eq}
+    Suppose $a,b,x,y \in \reals$.
+    Suppose $a < b$.
+    Suppose $x < y$.
+    If $a \leq x < b \leq y$ then $\intervalopen{a}{b} \inter \intervalopen{x}{y} = \intervalopen{x}{b}$.
+\end{lemma}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+\begin{lemma}\label{reals_order_total2}
+    For all $a,b \in \reals$ we have $a < b \lor a > b \lor a = b$.
+\end{lemma}
+
+
+\begin{theorem}\label{topological_basis_reals_is_basis}
+    $\topoBasisReals$ is a topological basis for $\reals$.
+\end{theorem}
+\begin{proof}
+    $\topoBasisReals$ is a topological prebasis for $\reals$ by \cref{topological_basis_reals_is_prebasis}.
+    Let $B = \topoBasisReals$.
+    It suffices to show that for all $U \in B$ we have for all $V \in B$ we have for all $x$ such that $x \in U, V$ there exists $W\in B$ such that $x\in W\subseteq U, V$.
+    Fix $U \in B$.
+    Fix $V \in B$.
+    It suffices to show that for all $x \in U \inter V$ there exists $W\in B$ such that $x\in W\subseteq U, V$.
+    Fix $x \in U \inter V$.
+    \begin{byCase}
+        \caseOf{$U \inter V = \emptyset$.}
+            Trivial.
+        \caseOf{$U \inter V \neq \emptyset$.}
+            Then $U \inter V$ is inhabited.
+            $x \in \reals$ by \cref{inter_lower_left,subseteq,topological_prebasis_iff_covering_family,omega_is_an_ordinal,naturals_subseteq_reals,subset_transitive,suc_subseteq_elim,ordinal_suc_subseteq}.
+            There exists $x_1, \alpha$ such that $x_1 \in \reals$ and $\alpha \in \realsplus$ and $\epsBall{x_1}{\alpha} = U$.
+            There exists $x_2, \beta$ such that $x_2 \in \reals$ and $\beta \in \realsplus$ and $\epsBall{x_2}{\beta} = V$.
+            Then $ (x_1 - \alpha) < x < (x_1 + \alpha)$.
+            Then $ (x_2 - \beta) < x < (x_2 + \beta)$.
+            Let $a = (x_1 - \alpha)$.
+            Let $b = (x_1 + \alpha)$.
+            Let $c = (x_2 - \beta)$.
+            Let $d = (x_2 + \beta)$.
+            We have $a < b$ and $a < x$ and $x < b$.
+            We have $c < d$ and $c < x$ and $x < d$.
+            We have $a \in \reals$.
+            We have $b \in \reals$.
+            We have $c \in \reals$.
+            We have $d \in \reals$.
+            We show that there exist $a',b'\in \reals$ such that $\intervalopen{a}{b} \inter \intervalopen{c}{d} = \intervalopen{a'}{b'}$.
+            \begin{subproof} 
+                \begin{byCase}
+                    \caseOf{$a < c$.}
+                        \begin{byCase}
+                            \caseOf{$b < d$.}
+                                Follows by \cref{intersection_openinterval_inclusion_of_border,intersection_openinterval_lower_border_eq,intersection_openinterval_none_border_eq,intersection_openinterval_upper_border_eq,reals_order_is_transitive,realsplus_in_reals_plus,realspuls_in_reals_minus}.
+                            \caseOf{$b = d$.}
+                                Follows by \cref{intersection_openinterval_inclusion_of_border,intersection_openinterval_lower_border_eq,intersection_openinterval_none_border_eq,intersection_openinterval_upper_border_eq,reals_order_is_transitive,realsplus_in_reals_plus,realspuls_in_reals_minus}.
+                            \caseOf{$b > d$.}
+                                Follows by \cref{intersection_openinterval_inclusion_of_border,intersection_openinterval_lower_border_eq,intersection_openinterval_none_border_eq,intersection_openinterval_upper_border_eq,reals_order_is_transitive,realsplus_in_reals_plus,realspuls_in_reals_minus}.
+                        \end{byCase}
+                    \caseOf{$a = c$.}
+                        \begin{byCase}
+                            \caseOf{$b < d$.}
+                                Follows by \cref{intersection_openinterval_inclusion_of_border,intersection_openinterval_lower_border_eq,intersection_openinterval_none_border_eq,intersection_openinterval_upper_border_eq,reals_order_is_transitive,realsplus_in_reals_plus,realspuls_in_reals_minus}.
+                            \caseOf{$b = d$.}
+                                Follows by \cref{intersection_openinterval_inclusion_of_border,intersection_openinterval_lower_border_eq,intersection_openinterval_none_border_eq,intersection_openinterval_upper_border_eq,reals_order_is_transitive,realsplus_in_reals_plus,realspuls_in_reals_minus}.
+                            \caseOf{$b > d$.}
+                                Follows by \cref{intersection_openinterval_inclusion_of_border,intersection_openinterval_lower_border_eq,intersection_openinterval_none_border_eq,intersection_openinterval_upper_border_eq,reals_order_is_transitive,realsplus_in_reals_plus,realspuls_in_reals_minus}.
+                        \end{byCase}
+                    \caseOf{$a > c$.}
+                        \begin{byCase}
+                            \caseOf{$b < d$.}
+                                Follows by \cref{intersection_openinterval_inclusion_of_border,intersection_openinterval_lower_border_eq,intersection_openinterval_none_border_eq,intersection_openinterval_upper_border_eq,reals_order_is_transitive,realsplus_in_reals_plus,realspuls_in_reals_minus,reals_add,minus_in_reals,realsplus,inter_comm,epsilon_ball}.
+                            \caseOf{$b = d$.}
+                                Follows by \cref{intersection_openinterval_inclusion_of_border,intersection_openinterval_lower_border_eq,intersection_openinterval_none_border_eq,intersection_openinterval_upper_border_eq,reals_order_is_transitive,realsplus_in_reals_plus,realspuls_in_reals_minus,reals_add,minus_in_reals,realsplus,inter_comm,epsilon_ball}.
+                            \caseOf{$b > d$.}
+                                Follows by \cref{intersection_openinterval_inclusion_of_border,intersection_openinterval_lower_border_eq,intersection_openinterval_none_border_eq,intersection_openinterval_upper_border_eq,reals_order_is_transitive,realsplus_in_reals_plus,realspuls_in_reals_minus,reals_add,minus_in_reals,realsplus,inter_comm,epsilon_ball}.
+                        \end{byCase}
+                \end{byCase}
+            \end{subproof}
+
+            Take $a',b'\in \reals$ such that $\intervalopen{a}{b} \inter \intervalopen{c}{d} = \intervalopen{a'}{b'}$.
+            We have $a',b' \in \reals$ by assumption.
+            We have $a' < b'$ by \cref{id_img,epsilon_ball,minus,intervalopen,reals_order_is_transitive}.
+            Then there exist $x',\epsilon'$ such that $x' \in \reals$ and $\epsilon' \in \realsplus$ and $\intervalopen{a'}{b'} = \epsBall{x'}{\epsilon'}$.
+            Then $x \in \epsBall{x'}{\epsilon'}$ by \cref{epsilon_ball}.
+
+            Follows by \cref{inter_lower_left,inter_lower_right,epsilon_ball,topological_basis_reals_eps_ball}.
+            %Then $(x_1 - \alpha) < (x_2 + \beta)$.
+
+            %Therefore $U \inter V = \intervalopen{}{(x_2 + \beta)}$.
+
+            %We show that if there exists $\delta \in \realsplus$ such that $\epsBall{x}{\delta} \subseteq U \inter V$ then there exists $W\in B$ such that $x\in W\subseteq U, V$.
+            %\begin{subproof}
+            %    Suppose there exists $\delta \in \realsplus$ such that $\epsBall{x}{\delta} \subseteq U \inter V$.
+            %    $x \in \epsBall{x}{\delta}$.
+            %    $\epsBall{x}{\delta} \subseteq U$.
+            %    $\epsBall{x}{\delta} \subseteq V$.
+            %    $\epsBall{x}{\delta} \in B$.
+            %\end{subproof}
+            %It suffices to show that there exists $\delta \in \realsplus$ such that $\epsBall{x}{\delta} \subseteq U \inter V$.
+
+
+            %It suffices to show that there exists $x_0, \delta$ such that $x_0 \in \reals$ and $\delta \in \realsplus$ and $\epsBall{x_0}{\delta} \subseteq u \inter V$.
+            %There exists $x_1, \alpha$ such that $x_1 \in \reals$ and $\alpha \in \realsplus$ and $\epsBall{x_1}{\alpha} = U$.
+            %There exists $x_2, \beta$ such that $x_2 \in \reals$ and $\beta \in \realsplus$ and $\epsBall{x_2}{\beta} = V$.
+            %Then $ (x_1 - \alpha) < x < (x_1 + \alpha)$.
+            %Then $ (x_2 - \beta) < x < (x_2 + \beta)$.
+            %\begin{byCase}
+            %    \caseOf{$x_1 = x_2$.}
+            %        Take $\gamma \in \realsplus$ such that either $\gamma = \alpha \land \gamma \leq \beta$ or $\gamma \leq \alpha \land \gamma = \beta$.
+            %    \caseOf{$x_1 < x_2$.}
+            %    \caseOf{$x_1 > x_2$.}
+            %\end{byCase}
+            %%Take $m$ such that $m \in \min{\{(x_1 + \alpha), (x_2 + \beta)\}}$.
+            %Take $n$ such that $n \in \max{\{(x_1 - \alpha), (x_2 - \beta)\}}$.
+            %Then $m < x < n$.
+            %We show that there exists $x_1 \in \reals$ such that $x_1 \in U \inter V$ and $x_1 < x$.
+            %\begin{subproof}
+            %    Suppose not.
+            %    Then For all $y \in U \inter V$ we have $x \leq y$.
+            %\end{subproof}
+            %We show that there exists $x_2 \in \reals$ such that $x_2 \in U \inter V$ and $x_2 > x$.
+            %\begin{subproof}
+            %    Trivial.
+            %\end{subproof}
+    \end{byCase}
+\end{proof}
+
+\begin{axiom}\label{topological_space_reals}
+    $\opens[\reals] = \genOpens{\topoBasisReals}{\reals}$.
+\end{axiom}
+
+\begin{theorem}\label{reals_is_topological_space}
+    $\reals$ is a topological space.
+\end{theorem}
+\begin{proof}
+    $\topoBasisReals$ is a topological basis for $\reals$.
+    Let $B = \topoBasisReals$.
+    We show that $\opens[\reals]$ is a family of subsets of $\carrier[\reals]$.
+    \begin{subproof}
+        It suffices to show that for all $A \in \opens[\reals]$ we have $A \subseteq \reals$.
+        Fix $A \in \opens[\reals]$.
+        Follows by \cref{powerset_elim,topological_space_reals,genopens}.
+    \end{subproof}
+    We show that $\reals \in\opens[\reals]$.
+    \begin{subproof}
+        $B$ covers $\reals$ by \cref{topological_prebasis_iff_covering_family,topological_basis}.
+        $\unions{B} \in \genOpens{B}{\reals}$.
+        $\reals \subseteq \unions{B}$.
+    \end{subproof}
+    We show that for all $A, B\in \opens[\reals]$ we have $A\inter B\in\opens[\reals]$.
+    \begin{subproof}
+        Follows by \cref{topological_space_reals,inters_in_genopens}.
+    \end{subproof}
+    We show that for all $F\subseteq \opens[\reals]$ we have $\unions{F}\in\opens[\reals]$.
+    \begin{subproof}
+        Follows by \cref{topological_space_reals,union_in_genopens}.
+    \end{subproof}
+    $\carrier[\reals] = \reals$.
+    Follows by \cref{topological_space}.
+\end{proof}
+
+\begin{proposition}\label{open_interval_is_open}
+    Suppose $a,b \in \reals$.
+    Then $\intervalopen{a}{b} \in \opens[\reals]$.
+\end{proposition}
+\begin{proof}
+    If $a > b$ then $\intervalopen{a}{b} = \emptyset$.
+    If $a = b$ then $\intervalopen{a}{b} = \emptyset$.
+    It suffices to show that if $a < b$ then $\intervalopen{a}{b} \in \opens[\reals]$.
+    Suppose $a \rless b$.
+    Take $x, \epsilon$ such that $x \in \reals$ and $\epsilon \in \realsplus$ and $\intervalopen{a}{b} = \epsBall{x}{\epsilon}$.
+    It suffices to show that $\epsBall{x}{\epsilon} \in \opens[\reals]$.
+    $\topoBasisReals$ is a topological basis for $\reals$.
+    $\epsBall{x}{\epsilon} \in \topoBasisReals$.
+    $\topoBasisReals \subseteq \opens[\reals]$ by \cref{basis_is_in_genopens,topological_space_reals,topological_basis_reals_is_basis}.
+\end{proof}
+
+\begin{lemma}\label{reals_minus_to_realsplus}
+    Suppose $a,b \in \reals$.
+    Suppose $a < b$.
+    Then $(b - a) \in \realsplus$.
+\end{lemma}
+
+\begin{lemma}\label{existence_of_epsilon_upper_border}
+    Suppose $a,b \in \reals$.
+    Suppose $a < b$.
+    Then there exists $\epsilon \in \realsplus$ such that $b \notin \epsBall{a}{\epsilon}$. 
+\end{lemma}
+\begin{proof}
+    Let $\epsilon = b - a$.
+    Then $\epsilon \in \realsplus$.
+    It suffices to show that $b \notin \epsBall{a}{\epsilon}$ by \cref{epsilon_ball,reals_addition_minus_behavior2,realsplus,minus,intervalopen,order_reals_lemma0}.
+    Suppose not.
+    Then $ b \in \epsBall{a}{\epsilon}$.
+    Therefore $ (a - \epsilon) < b < (a + \epsilon)$.
+    $b = (a + \epsilon)$.
+    Contradiction.
+\end{proof}
+
+\begin{lemma}\label{existence_of_epsilon_lower_border}
+    Suppose $a,b \in \reals$.
+    Suppose $a > b$.
+    Then there exists $\epsilon \in \realsplus$ such that $b \notin \epsBall{a}{\epsilon}$. 
+\end{lemma}
+\begin{proof}
+    Let $\epsilon = a - b$.
+    Then $\epsilon \in \realsplus$.
+    It suffices to show that $b \notin \epsBall{a}{\epsilon}$ by \cref{epsilon_ball,reals_addition_minus_behavior2,realsplus,minus,intervalopen,order_reals_lemma0}.
+    Suppose not.
+    Then $ b \in \epsBall{a}{\epsilon}$.
+    Therefore $ (a - \epsilon) < b < (a + \epsilon)$.
+    $b = (a - \epsilon)$.
+    Contradiction.
+\end{proof}
+
+\begin{proposition}\label{openinterval_infinite_left_in_opens}
+    Suppose $a \in \reals$.
+    Then $\intervalopenInfiniteLeft{a} \in \opens[\reals]$.
+\end{proposition}
+\begin{proof}
+    Let $E = \{ B \in \pow{\reals} \mid \exists x \in \intervalopenInfiniteLeft{a} . \exists \delta \in \realsplus . B = \epsBall{x}{\delta} \land a \notin \epsBall{x}{\delta}  \}$.
+    We show that for all $x \in \intervalopenInfiniteLeft{a}$ we have there exists $e \in E$ such that $x \in e$.
+    \begin{subproof}
+        Fix $x \in \intervalopenInfiniteLeft{a}$.
+        Then $x < a$.
+        Take $\delta' \in \realsplus$ such that $a \notin \epsBall{x}{\delta'}$.
+        $x \in \epsBall{x}{\delta'}$ by \cref{intervalopen,epsilon_ball,reals_addition_minus_behavior1,reals_order_minus_positiv,minus,reals_add,realsplus,intervalopen_infinite_left}.
+        $a \notin \epsBall{x}{\delta'}$.
+        $\epsBall{x}{\delta'} \in E$.
+    \end{subproof}
+    $E \subseteq \topoBasisReals$.
+    We show that $\unions{E} = \intervalopenInfiniteLeft{a}$.
+    \begin{subproof}
+        We show that $\unions{E} \subseteq \intervalopenInfiniteLeft{a}$.
+        \begin{subproof}
+            It suffices to show that for all $x \in \unions{E}$ we have $x \in \intervalopenInfiniteLeft{a}$.
+            Fix $x \in \unions{E}$.
+            Take $e \in E$ such that $x \in e$ by \cref{unions_iff}.
+            $x \in \reals$.
+            Take $x',\delta'$ such that $x' \in \reals$ and $\delta' \in \realsplus$ and $e = \epsBall{x'}{\delta'}$ by \cref{epsilon_ball,minus,topo_basis_reals_eps_iff,setminus,setminus_emptyset,elem_subseteq}.
+            $\epsBall{x'}{\delta'} \in E$.
+            We show that for all $y \in e$ we have $y < a$.
+            \begin{subproof}
+                Fix $y \in e$.
+                Then $y \in \epsBall{x'}{\delta'}$.
+                $e = \epsBall{x'}{\delta'}$.
+                There exists $x'' \in \intervalopenInfiniteLeft{a}$ such that there exists $\delta'' \in \realsplus$ such that $e = \epsBall{x''}{\delta''}$ and $a \notin \epsBall{x''}{\delta''}$.
+                Take $x'',\delta''$ such that $x'' \in \intervalopenInfiniteLeft{a}$ and $\delta'' \in \realsplus$ and $e = \epsBall{x''}{\delta''}$ and $a \notin \epsBall{x''}{\delta''}$.
+                Suppose not.
+                Take $y' \in e$ such that $y' > a$. 
+                $x'' < a$.
+                $(x'' - \delta'') < y' < (x'' + \delta'')$ by \cref{minus,intervalopen,epsilon_ball,realsplus,reals_add,reals_addition_minus_behavior1,reals_order_minus_positiv}.
+                $(x'' - \delta'') < x'' < (x'' + \delta'')$ by \cref{minus,intervalopen,epsilon_ball,realsplus,reals_add,reals_addition_minus_behavior1,reals_order_minus_positiv}.
+                Then $x'' < a < y'$.
+                Therefore $(x'' - \delta'') < a < (x'' + \delta'')$ by \cref{realspuls_in_reals_minus,intervalopen_infinite_left,reals_order_is_transitive,reals_add,realsplus_in_reals,powerset_elim,subseteq}.
+                Then $a \in e$ by \cref{epsball_are_connected_in_reals,intervalopen_infinite_left,neq_witness}.
+                Contradiction.
+            \end{subproof}
+            $x < a$.
+            Then $x \in \intervalopenInfiniteLeft{a}$.
+        \end{subproof}
+        We show that $\intervalopenInfiniteLeft{a} \subseteq \unions{E}$.
+        \begin{subproof}
+            Trivial.
+        \end{subproof}
+    \end{subproof}
+    $\unions{E} \in \opens[\reals]$ by \cref{opens_unions,reals_is_topological_space,basis_is_in_genopens,topological_space_reals,topological_basis_reals_is_basis,subset_transitive}.
+\end{proof}
+
+\begin{lemma}\label{continuous_on_basis_implies_continuous_endo}
+    Suppose $X$ is a topological space.
+    Suppose $B$ is a topological basis for $X$.
+    Suppose $f$ is a function from $X$ to $X$.
+    $f$ is continuous iff for all $b \in B$ we have $\preimg{f}{b} \in \opens[X]$.
+\end{lemma}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+\begin{proposition}\label{openinterval_infinite_right_in_opens}
+    Suppose $a \in \reals$.
+    Then $\intervalopenInfiniteRight{a} \in \opens[\reals]$.
+\end{proposition}
+\begin{proof}
+    Let $E = \{ B \in \pow{\reals} \mid \exists x \in \intervalopenInfiniteRight{a} . \exists \delta \in \realsplus . B = \epsBall{x}{\delta} \land a \notin \epsBall{x}{\delta}  \}$.
+    We show that for all $x \in \intervalopenInfiniteRight{a}$ we have there exists $e \in E$ such that $x \in e$.
+    \begin{subproof}
+        Fix $x \in \intervalopenInfiniteRight{a}$.
+        Then $a < x$.
+        Take $\delta' \in \realsplus$ such that $a \notin \epsBall{x}{\delta'}$.
+        $x \in \epsBall{x}{\delta'}$ by \cref{intervalopen,epsilon_ball,reals_addition_minus_behavior1,reals_order_minus_positiv,minus,reals_add,realsplus,intervalopen_infinite_right}.
+        $a \notin \epsBall{x}{\delta'}$.
+        $\epsBall{x}{\delta'} \in E$.
+    \end{subproof}
+    $E \subseteq \topoBasisReals$.
+    We show that $\unions{E} = \intervalopenInfiniteRight{a}$.
+    \begin{subproof}
+        We show that $\unions{E} \subseteq \intervalopenInfiniteRight{a}$.
+        \begin{subproof}
+            It suffices to show that for all $x \in \unions{E}$ we have $x \in \intervalopenInfiniteRight{a}$.
+            Fix $x \in \unions{E}$.
+            Take $e \in E$ such that $x \in e$ by \cref{unions_iff}.
+            $x \in \reals$.
+            Take $x',\delta'$ such that $x' \in \reals$ and $\delta' \in \realsplus$ and $e = \epsBall{x'}{\delta'}$ by \cref{epsilon_ball,minus,topo_basis_reals_eps_iff,setminus,setminus_emptyset,elem_subseteq}.
+            $\epsBall{x'}{\delta'} \in E$.
+            We show that for all $y \in e$ we have $y > a$.
+            \begin{subproof}
+                Fix $y \in e$.
+                Then $y \in \epsBall{x'}{\delta'}$.
+                $e = \epsBall{x'}{\delta'}$.
+                There exists $x'' \in \intervalopenInfiniteRight{a}$ such that there exists $\delta'' \in \realsplus$ such that $e = \epsBall{x''}{\delta''}$ and $a \notin \epsBall{x''}{\delta''}$.
+                Take $x'',\delta''$ such that $x'' \in \intervalopenInfiniteRight{a}$ and $\delta'' \in \realsplus$ and $e = \epsBall{x''}{\delta''}$ and $a \notin \epsBall{x''}{\delta''}$.
+                Suppose not.
+                Take $y' \in e$ such that $y' < a$ by \cref{reals_order_total,intervalopen,eps_ball_implies_open_interval}. 
+                $x'' > a$.
+                $(x'' - \delta'') < y' < (x'' + \delta'')$ by \cref{minus,intervalopen,intervalclosed,epsilon_ball,realsplus,reals_add,reals_addition_minus_behavior1,reals_order_minus_positiv}.
+                $(x'' - \delta'') < x'' < (x'' + \delta'')$ by \cref{minus,intervalopen,intervalclosed,epsilon_ball,realsplus,reals_add,reals_addition_minus_behavior1,reals_order_minus_positiv}.
+                Then $x'' > a > y'$.
+                Therefore $(x'' - \delta'') > a > (x'' + \delta'')$ by \cref{realspuls_in_reals_minus,intervalopen_infinite_right,reals_order_is_transitive,reals_add,realsplus_in_reals,powerset_elim,subseteq,epsball_are_connected_in_reals,subseteq}.
+                Then $a \in e$ by \cref{reals_order_is_transitive,reals_order_total,reals_add,realsplus,epsball_are_connected_in_reals,intervalopen_infinite_right,neq_witness}.
+                Contradiction.
+            \end{subproof}
+            $x > a$.
+            Then $x \in \intervalopenInfiniteRight{a}$.
+        \end{subproof}
+        We show that $\intervalopenInfiniteRight{a} \subseteq \unions{E}$.
+        \begin{subproof}
+            Trivial.
+        \end{subproof}
+    \end{subproof}
+    $\unions{E} \in \opens[\reals]$.
+
+    %Let $I = \{\neg{b} \mid b \in \intervalopenInfiniteRight{a} \}$.
+    %Let $f(x) = \neg{x}$ for $x \in \reals$.
+    %$f$ is a function from $\reals$ to $\reals$.
+    %We show that $f$ is continuous.
+    %\begin{subproof}
+    %    It suffices to show that for all $b \in \topoBasisReals$ we have $\preimg{f}{b} \in \opens[\reals]$.
+    %    Fix $b \in \topoBasisReals$.
+    %    Take $x, \epsilon$ such that $x \in \reals$ and $\epsilon \in \realsplus$ and $b = \epsBall{x}{\epsilon}$.
+    %    Let $y = \neg{x}$.
+    %    It suffices to show that $\preimg{f}{b} \in \topoBasisReals$ by \cref{topological_space_reals,topological_basis_reals_is_basis,basis_is_in_genopens,cons_remove,cons_subseteq_iff}.
+    %    It suffices to show that $\epsBall{y}{\epsilon} = \preimg{f}{\epsBall{x}{\epsilon}}$.
+    %    $\preimg{f}{\epsBall{x}{\epsilon}} \subseteq \reals$.
+    %    $\epsBall{y}{\epsilon} \subseteq \reals$ by \cref{intervalopen,subseteq,minus,epsilon_ball}.
+    %    %It suffices to show that for all $x \in \reals$ we have $x \in \epsBall{y}{\epsilon}$ iff $x \in \preimg{f}{\epsBall{x}{\epsilon}}$.
+    %    %Fix $x \in \reals$.
+    %    Let $u = (y - \epsilon)$.
+    %    Let $v = (y + \epsilon)$.
+    %    $u = \neg{(x - \epsilon)}$.
+    %    $v = \neg{(x + \epsilon)}$.
+    %    %$v - u = \epsilon + \epsilon$.
+    %    We show that for all $z \in \epsBall{y}{\epsilon}$ we have $z \in \preimg{f}{\epsBall{x}{\epsilon}}$.
+    %    \begin{subproof}
+    %        Fix $z \in \epsBall{y}{\epsilon}$.
+    %        Then $u < z < v$.
+    %        Let $z' = z - u$.
+    %        Then $z = u + z'$.
+    %        Suppose not.
+    %        Let $h = \neg{z}$.
+    %        $\neg{h} = \neg{\neg{z}}$.
+    %        $\neg{h} = z$.
+    %        Then $f(h) = \neg{h}$.
+    %        $f(h) = z$.
+    %        Then $z \in \preimg{f}{\{h\}}$.
+%
+    %    \end{subproof}
+    %    We show that for all $z \in \preimg{f}{\epsBall{x}{\epsilon}}$ we have $z \in \epsBall{y}{\epsilon}$.
+    %    \begin{subproof}
+    %        Fix $z \in \preimg{f}{\epsBall{x}{\epsilon}}$.
+    %        Take $h \in \epsBall{x}{\epsilon}$ such that $f(h) = z$.
+    %    \end{subproof}
+    %    Follows by set extensionality.
+    %\end{subproof}
+    %$\intervalopenInfiniteLeft{a} \in \opens[\reals]$.
+    %We show that $\preimg{f}{\intervalopenInfiniteLeft{a}} = \intervalopenInfiniteRight{a}$.
+    %\begin{subproof}
+    %    Omitted.
+    %\end{subproof}
+    %Then $\intervalopenInfiniteRight{a} \in \opens[\reals]$ by \cref{continuous,preim_eq_img_of_converse,openinterval_infinite_left_in_opens}.
+\end{proof}
+
+\begin{lemma}\label{reals_as_union_of_open_closed_intervals1}
+    Suppose $a,b \in \reals$.
+    Then $\reals = \intervalopenInfiniteLeft{a} \union \intervalopenInfiniteRight{b} \union \intervalclosed{a}{b}$.
+\end{lemma}
+\begin{proof}
+    We show that for all $x \in \reals$ we have $x \in (\intervalopenInfiniteLeft{a} \union \intervalopenInfiniteRight{b} \union \intervalclosed{a}{b})$.
+    \begin{subproof}
+        Fix $x \in \reals$.
+        Follows by \cref{union_intro_left,intervalopen_infinite_left,reals_order_total,reals_order_total2,union_iff,intervalopen_infinite_right,union_assoc,union_intro_right,intervalclosed}.
+    \end{subproof}
+\end{proof}
+
+\begin{lemma}\label{reals_as_union_of_open_closed_intervals2}
+    Suppose $a \in \reals$.
+    Then $\reals = \intervalopenInfiniteLeft{a} \union \intervalclosedInfiniteRight{a}$.
+\end{lemma}
+\begin{proof}
+    It suffices to show that for all $x \in \reals$ we have either $x \in \intervalopenInfiniteLeft{a}$ or $x \in \intervalclosedInfiniteRight{a}$ by \cref{intervalopen_infinite_left,union_intro_left,neq_witness,intervalclosed_infinite_right,union_intro_right,union_iff}.
+    Trivial.
+\end{proof}
+
+\begin{lemma}\label{reals_as_union_of_open_closed_intervals3}
+    Suppose $a \in \reals$.
+    Then $\reals = \intervalopenInfiniteRight{a} \union \intervalclosedInfiniteLeft{a}$.
+\end{lemma}
+\begin{proof}
+    It suffices to show that for all $x \in \reals$ we have either $x \in \intervalclosedInfiniteLeft{a}$ or $x \in \intervalopenInfiniteRight{a}$.
+    Trivial.
+\end{proof}
+
+\begin{lemma}\label{intersection_of_open_closed__infinite_intervals_open_right}
+    Suppose $a \in \reals$.
+    Then $\intervalopenInfiniteRight{a} \inter \intervalclosedInfiniteLeft{a} = \emptyset$.
+\end{lemma}
+\begin{proof}
+    Follows by \cref{reals_order_total,inter_lower_left,intervalopen_infinite_right,order_reals_lemma6,inter_lower_right,foundation,subseteq,intervalclosed_infinite_left}.
+\end{proof}
+
+\begin{lemma}\label{intersection_of_open_closed__infinite_intervals_open_left}
+    Suppose $a \in \reals$.
+    Then $\intervalopenInfiniteLeft{a} \inter \intervalclosedInfiniteRight{a} = \emptyset$.
+\end{lemma}
+
+\begin{proposition}\label{closedinterval_infinite_right_in_closeds}
+    Suppose $a \in \reals$.
+    Then $\intervalclosedInfiniteRight{a} \in \closeds{\reals}$.
+\end{proposition}
+\begin{proof}
+    $\intervalclosedInfiniteRight{a} = \reals \setminus \intervalopenInfiniteLeft{a}$ by \cref{intersection_of_open_closed__infinite_intervals_open_left,reals_as_union_of_open_closed_intervals2,setminus_inter,double_relative_complement,subseteq_union_setminus,subseteq_setminus,setminus_union,setminus_disjoint,setminus_partition,setminus_subseteq,setminus_emptyset,setminus_self,setminus_setminus,double_complement_union}.
+\end{proof}
+
+\begin{proposition}\label{closedinterval_infinite_left_in_closeds}
+    Suppose $a \in \reals$.
+    Then $\intervalclosedInfiniteLeft{a} \in \closeds{\reals}$.
+\end{proposition}
+\begin{proof}
+    $\intervalclosedInfiniteLeft{a} = \reals \setminus \intervalopenInfiniteRight{a}$.
+\end{proof}
+
+\begin{proposition}\label{closedinterval_eq_openintervals_setminus_reals}
+    Suppose $a,b \in \reals$.
+    Then $\reals \setminus (\intervalopenInfiniteLeft{a} \union \intervalopenInfiniteRight{b}) = \intervalclosed{a}{b}$.
+\end{proposition}
+\begin{proof}
+    We have $\intervalclosed{a}{b} \subseteq \reals$.
+    We show that $\reals \setminus (\intervalopenInfiniteLeft{a} \union \intervalopenInfiniteRight{b}) = (\reals \setminus \intervalopenInfiniteLeft{a}) \inter (\reals \setminus \intervalopenInfiniteRight{b})$.
+    \begin{subproof}
+        We show that for all $x \in \reals \setminus (\intervalopenInfiniteLeft{a} \union \intervalopenInfiniteRight{b})$ we have $x \in (\reals \setminus \intervalopenInfiniteLeft{a}) \inter (\reals \setminus \intervalopenInfiniteRight{b})$.
+        \begin{subproof}
+            Fix $x \in \reals \setminus (\intervalopenInfiniteLeft{a} \union \intervalopenInfiniteRight{b})$.
+            Then $x \in \reals \setminus \intervalopenInfiniteLeft{a}$ by \cref{setminus,double_complement_union}.
+            Then $x \in \reals \setminus \intervalopenInfiniteRight{b}$ by \cref{union_upper_left,subseteq,union_comm,subseteq_implies_setminus_supseteq}.
+            Follows by \cref{inter_intro}.
+        \end{subproof}
+        We show that for all $x \in (\reals \setminus \intervalopenInfiniteLeft{a}) \inter (\reals \setminus \intervalopenInfiniteRight{b})$ we have $x \in \reals \setminus (\intervalopenInfiniteLeft{a} \union \intervalopenInfiniteRight{b})$.
+        \begin{subproof}
+            Fix $x \in (\reals \setminus \intervalopenInfiniteLeft{a}) \inter (\reals \setminus \intervalopenInfiniteRight{b})$.
+            Then $x \in (\reals \setminus \intervalopenInfiniteLeft{a})$ by \cref{setminus_setminus,setminus}.
+            Then $x \in (\reals \setminus \intervalopenInfiniteRight{b})$ by \cref{inter_lower_right,elem_subseteq,setminus_setminus}.
+        \end{subproof}
+        Follows by \cref{setminus_union}.
+    \end{subproof}
+    We show that $\reals \setminus \intervalopenInfiniteLeft{a} = \intervalclosedInfiniteRight{a}$.
+    \begin{subproof}
+        For all $x \in \intervalclosedInfiniteRight{a}$ we have $x \geq a$.
+        For all $x \in (\reals \setminus \intervalopenInfiniteLeft{a})$ we have $x \geq a$.
+        Follows by set extensionality.
+    \end{subproof}
+    $\reals \setminus \intervalopenInfiniteRight{b} = \intervalclosedInfiniteLeft{b}$.
+    It suffices to show that $\intervalclosedInfiniteLeft{b} \inter \intervalclosedInfiniteRight{a} = \intervalclosed{a}{b}$.
+    For all $x \in \intervalclosed{a}{b}$ we have $a \leq x \leq b$.
+    For all $x \in (\intervalclosedInfiniteLeft{b} \inter \intervalclosedInfiniteRight{a})$ we have $a \leq x \leq b$.
+    Follows by set extensionality.
+\end{proof}
+
+\begin{proposition}\label{closedinterval_is_closed}
+    Suppose $a,b \in \reals$.
+    Then $\intervalclosed{a}{b} \in \closeds{\reals}$.
+\end{proposition}
+\begin{proof}
+    We have $\reals = \intervalopenInfiniteLeft{a} \union \intervalopenInfiniteRight{b} \union \intervalclosed{a}{b}$.
+    It suffices to show that $\reals \setminus (\intervalopenInfiniteLeft{a} \union \intervalopenInfiniteRight{b}) = \intervalclosed{a}{b}$ by \cref{closeds,setminus_subseteq,powerset_intro,closed_minus_open_is_closed,opens_type,subseteq_refl,union_open,is_closed_in,reals_carrier_reals,setminus_self,emptyset_open,reals_is_topological_space,openinterval_infinite_left_in_opens,openinterval_infinite_right_in_opens}.
+\end{proof}
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
new file mode 100644
index 0000000..cd85fbc
--- /dev/null
+++ b/library/topology/urysohn.tex
@@ -0,0 +1,924 @@
+\import{topology/topological-space.tex}
+\import{topology/separation.tex}
+\import{topology/continuous.tex}
+\import{topology/basis.tex}
+\import{numbers.tex}
+\import{function.tex}
+\import{set.tex}
+\import{cardinal.tex}
+\import{relation.tex}
+\import{relation/uniqueness.tex}
+\import{set/cons.tex}
+\import{set/powerset.tex}
+\import{set/fixpoint.tex}
+\import{set/product.tex}
+
+\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.
+%           The limit of our chain turns out to be our desired continuous function from a topological space $X$ to $[0,1]$.
+%           With the property that \[f\mid_{A}=1 \land f\mid_{B}=0\] for \[A,B\] closed sets.
+
+%Chains of  sets.
+
+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$.
+
+%           As Jänich propose we want a special property on chains of subsets.
+%           We need a rising chain of subsets $\mathfrak{A} = (A_{0}, ... ,A_{r})$ of $A$, i.e. 
+%           \begin{align}
+%               A = A_{0} \subset A_{1} \subset ... \subset A_{r} \subset X\setminus B 
+%           \end{align} 
+%           such that for all elements in this chain following holds, 
+%           $\overline{A_{i-1}}  \subset \interior{A_{i}}$. 
+%           In this case we call the chain legal.
+
+\begin{definition}\label{urysohnone_one_to_n_set}
+    $\seq{m}{n} = \{x \in \naturals \mid  m \leq x \leq n\}$.   
+\end{definition}
+
+
+
+%%-----------------------
+%   Idea:
+%   A sequence could be define as a family of sets, 
+%   together with the existence of an indexing function.
+%
+%%-----------------------
+\begin{struct}\label{urysohnone_sequence}
+    A sequence $X$ is a onesorted structure equipped with
+    \begin{enumerate}
+        \item $\indexx$
+        \item $\indexxset$
+        
+    \end{enumerate}
+    such that
+    \begin{enumerate}
+        \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}
+
+% Eine folge ist ein Funktion mit domain \subseteq Ordinal zahlen 
+
+
+
+
+\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{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]$.
+\end{definition}
+
+
+
+% TODO: The Notion above should be generalised to sequences since we need them as well for our limit
+% and also for the subproof of continuity of the limit.
+
+
+%     \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
+%         %for all $x,y \in C$ we have if $f(x) < f(y)$ then $x \subset y \land \closure{x} \subset \interior{y}$.
+%     \end{definition}
+
+% TODO: We need a notion for declarinf new properties to existing thing. 
+%
+% The following gives a example and a wish want would be nice to have:
+% "A (structure) is called (adjectiv of property), if"
+%
+% This should then be use als follows:
+% Let $X$ be a (adjectiv_1) ... (adjectiv_n) (structure_word). 
+% Which should be translated to fol like this:
+% ?[X]: is_structure(X) & is_adjectiv_1(X) & ... & is_adjectiv_n(X)
+% ---------------------------------------------------------------
+
+
+
+\subsection{staircase function}
+
+\begin{definition}\label{urysohnone_minimum}
+    $\min{X} = \{x \in X \mid \forall y \in X. x \leq y \}$.
+\end{definition}
+
+\begin{definition}\label{urysohnone_maximum}
+    $\max{X} = \{x \in X \mid \forall y \in X. x \geq y \}$.
+\end{definition}
+
+\begin{definition}\label{urysohnone_intervalclosed}
+    $\intervalclosed{a}{b} = \{x \in \reals \mid a \leq x \leq b\}$.
+\end{definition}
+
+\begin{definition}\label{urysohnone_intervalopen}
+    $\intervalopen{a}{b} = \{ x \in \reals \mid a < x < b\}$.
+\end{definition}
+
+
+\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{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{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{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$
+    we have there exist $A',B' \in \opens[X]$
+    such that  $A \subseteq A'$ and $B \subseteq B'$ and $A' \inter B' = \emptyset$.    
+\end{abbreviation}
+
+\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{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{urysohnone_infinte_sequence}
+    $S$ is a infinite sequence iff $S$ is a sequence and $\indexxset[S]$ is infinite.
+\end{abbreviation}
+
+\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{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{urysohnone_two}
+    $\two = \suc{1}$.
+\end{abbreviation}
+
+\begin{lemma}\label{urysohnone_two_in_reals}
+    $\two \in \reals$.
+\end{lemma}
+
+\begin{lemma}\label{urysohnone_two_in_naturals}
+    $\two \in \naturals$.
+\end{lemma}
+
+\begin{inductive}\label{urysohnone_power_of_two}
+    Define $\powerOfTwoSet \subseteq (\naturals \times \naturals)$.
+    \begin{enumerate}
+        \item  $(\zero, 1) \in \powerOfTwoSet$.
+        \item  If $(m,k) \in \powerOfTwoSet$, then $(m+1, k \rmul \two) \in \powerOfTwoSet$.
+    \end{enumerate}
+\end{inductive}
+
+\begin{abbreviation}\label{urysohnone_pot}
+    $\pot = \powerOfTwoSet$.
+\end{abbreviation}
+
+\begin{lemma}\label{urysohnone_dom_pot}
+    $\dom{\pot} = \naturals$.
+\end{lemma}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+\begin{lemma}\label{urysohnone_ran_pot}
+    $\ran{\pot} \subseteq \naturals$.
+\end{lemma}
+
+
+\begin{axiom}\label{urysohnone_pot1}
+    $\pot \in \funs{\naturals}{\naturals}$.
+\end{axiom}
+
+\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{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{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{urysohnone_urysohn_set_in_between}
+    Let $X$ be a urysohn space.
+    Suppose $A,B \in \closeds{X}$.
+    Suppose $A \subset B$.
+    %Suppose $B \union A \neq \carrier[X]$.
+    There exist $C \in \closeds{X}$
+    such that $A \subset C \subset B$ or $A, B \in \opens[X]$.
+\end{lemma}
+\begin{proof}
+    We have $B \setminus A$ is inhabited.
+    Take $x$ such that $x \in (B \setminus A)$.
+    Then $A \subset (A \union \{x\})$.
+    Let $C = \closure{A \union \{x\}}{X}$.
+    We have $(A \union \{x\}) \subseteq \closure{A \union \{x\}}{X}$.
+    Therefore $A \subset C$.
+    $A \subseteq B \subseteq \carrier[X]$.
+    $x \in B$.
+    Therefore $x \in \carrier[X]$.
+    $(A \union \{x\}) \subseteq \carrier[X]$.
+    We have $\closure{A \union \{x\}}{X}$ is closed in $X$ by \cref{closure_is_closed}.
+    Therefore $C$ is closed in $X$ by \cref{closure_is_closed}.
+    \begin{byCase}
+        \caseOf{$C = B$.}
+            %We have $\carrier[X] \setminus A$ is open in $X$.    
+            %We have $\carrier[X] \setminus B$ is open in $X$.
+            %$\{x\}$ is closed in $X$.% by \cref{hausdorff_implies_singltons_closed}.
+            %$A \union \{x\} = C$.
+            %$\carrier[X] \setminus (A \union \{x\}) = (\carrier[X] \setminus C)$.
+            %$\carrier[X] \setminus (A) = \{x\} \union (\carrier[X] \setminus C)$.
+
+
+            %Therefore $\{x\}$ is open in $X$.
+            Omitted.
+        \caseOf{$C \neq B$.}
+            Omitted.
+    \end{byCase}
+
+\end{proof}
+
+
+\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.
+    Then there exist $U$
+    such that $\carrier[U] = \{A,(\carrier[X] \setminus B)\}$
+    and $\indexxset[U]= \{\zero, 1\}$
+    and $\indexx[U](\zero) = A$
+    and $\indexx[U](1) = (\carrier[X] \setminus B)$.
+    %$U$ is a urysohnchain in $X$.
+\end{proposition}
+\begin{proof}
+
+    Omitted.
+
+    %   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 \indexxset[U]$ we have $n = \zero \lor n = 1$.
+    %       It suffices to show that for all $n \in \indexxset[U]$ we have
+    %       for all $m \in \indexxset[U]$ such that 
+    %       $n < m$ we have $\indexx[U](n) \subseteq \indexx[U](m)$.
+    %       Fix $n \in \indexxset[U]$.
+    %       Fix $m \in \indexxset[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 \indexxset[U]$ such that $n < m$ we have
+    %   $\closure{\indexx[U](n)}{X} \subseteq \interior{\indexx[U](m)}{X}$.
+    %   \begin{subproof}
+    %       Omitted.
+    %   \end{subproof}
+
+    
+\end{proof}
+
+\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.
+    Suppose there exist $U$
+    such that $\carrier[U] = \{A,(\carrier[X] \setminus B)\}$
+    and $\indexxset[U]= \{\zero, 1\}$
+    and $\indexx[U](\zero) = A$
+    and $\indexx[U](1) = (\carrier[X] \setminus B)$.
+    Then $U$ is a urysohnchain in $X$.
+\end{proposition}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+
+
+\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 
+    $\closure{A}{X} \subseteq \interior{C}{X} \subseteq \closure{C}{X} \subseteq \interior{B}{X}$.
+\end{proposition}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+
+
+\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$.
+\end{proposition}
+\begin{proof}
+    % U  = ( A_{0}, A_{1}, A_{2}, ... , A_{n-1}, A_{n})
+    % U' = ( A_{0}, A'_{1}, A_{1}, A'_{2}, A_{2}, ...   A_{n-1}, A'_{n}, A_{n})
+
+    % Let $m = \max{\indexxset[U]}$.
+    % For all $n \in (\indexxset[U] \setminus \{m\})$ we have there exist $C \subseteq X$ 
+    % 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{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$
+    %    and for all $g \in C'$ such that $g \neq c$ we have not $y \subset g \subset x$.
+    %\end{definition}
+    Omitted.
+
+\end{proof}
+
+
+
+
+
+\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$.
+    Then there exist $f$ such that $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ 
+    and for all $n \in \indexxset[U]$ we have for all $x \in \indexx[U](n)$ 
+    we have $f(x) = \rfrac{n}{k}$.
+\end{proposition}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+\begin{abbreviation}\label{urysohnone_refinment_abbreviation}
+    $x \refine y$ iff $x$ is a refinmant of $y$.
+\end{abbreviation}
+
+
+
+
+
+\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{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{urysohnone_abs_behavior1}
+    If $x \geq \zero$ then $\abs{x} = x$.
+\end{axiom}
+
+\begin{axiom}\label{urysohnone_abs_behavior2}
+    If $x < \zero$ then $\abs{x} = \neg{x}$.
+\end{axiom}
+
+\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
+    there exist $N \in \indexxset[s]$ such that
+    for all $m \in \indexxset[s]$ such that $m > N$ 
+    we have $\abs{\indexx[s](N) - \indexx[s](m)} < \epsilon$.
+\end{abbreviation}
+
+
+\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$
+    we have there exist $n \in \indexxset[s]$ such that 
+    for all $m \in \indexxset[s]$ such that $m > n$ 
+    we have $\abs{x - \indexx[s](n)} < \epsilon$.
+\end{definition}
+
+\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$.
+\end{proposition}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+\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{urysohnone_realsminus}
+    $\realsminus = \{r \in \reals \mid r < \zero\}$.
+\end{definition}
+
+\begin{abbreviation}\label{urysohnone_realsplus}
+    $\realsplus = \reals \setminus \realsminus$.
+\end{abbreviation}
+
+\begin{proposition}\label{urysohnone_intervalclosed_subseteq_reals}
+    Suppose $a,b \in \reals$.
+    Suppose $a < b$.
+    Then $\intervalclosed{a}{b} \subseteq \reals$.
+\end{proposition}
+
+
+
+\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}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+\begin{lemma}\label{urysohnone_frection2}
+    Suppose $a,b \in \reals$.
+    Suppose $a < b$.
+    Then $\intervalopen{a}{b}$ is infinite.
+\end{lemma}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+\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$. 
+\end{lemma}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+\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)}$.
+\end{proposition}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+\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)}$.
+\end{proposition}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+\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{urysohnone_epsilonball}
+    $\epsBall{a}{\epsilon}  = \intervalopen{(a - \epsilon)}{(a + \epsilon)}$.
+\end{abbreviation}
+
+\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}$.
+\end{proposition}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+
+
+ 
+%\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{urysohnone_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{urysohnone_urysohn1}
+    Let $X$ be a urysohn space.
+    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.
+\end{theorem}
+\begin{proof}
+    
+    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{urysohnone_urysohnchain_induction_begin}.
+    
+    We show that there exist $\zeta$ such that $\zeta$ is a sequence 
+    and $\indexxset[\zeta] = \naturals$
+    and $\eta \in \carrier[\zeta]$ and $\indexx[\zeta](\eta) = \zero$
+    and for all $n \in \indexxset[\zeta]$ we have $n+1 \in \indexxset[\zeta]$ 
+    and $\indexx[\zeta](n+1)$ is a refinmant of $\indexx[\zeta](n)$.
+    \begin{subproof}
+            %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)))\}$.
+            %
+            %    % TODO: Proof that \beta is a function which would be used for the indexing.
+            %For all $n \in \naturals$ we have there exist $x \in \alpha$ such that $(n,x) \in \beta$.
+            %$\dom{\beta} = \naturals$.
+            %$\ran{\beta} = \alpha$.
+            %$\beta \in \funs{\naturals}{\alpha}$.
+            %Take $\zeta$ such that $\carrier[\zeta] = \alpha$ and $\indexxset[\zeta] = \naturals$ and $\indexx[\zeta] = \beta$.
+        Omitted.
+    \end{subproof}
+
+    Let $\alpha = \carrier[X]$.
+    %Define $f : \alpha \to \naturals$ such that $f(x) =$
+    %\begin{cases}
+    %    & 1        & \text{if} x \in A \lor x \in B 
+    %    & k     & \text{if} \exists k \in \naturals 
+    %\end{cases}
+%
+    %We show that there exist $k \in \funs{\carrier[X]}{\reals}$ such that
+    %$k(x)$
+
+    %For all $n \in \naturals$ we have $\indexx[\zeta](n)$ is a urysohnchain in $X$.
+
+    We show that for all $n \in \indexxset[\zeta]$ we have $\indexx[\zeta](n)$ has cardinality $\pot(n)$.
+    \begin{subproof}
+        Omitted.
+    \end{subproof}
+
+    We show that for all $m \in \indexxset[\zeta]$ we have $\pot(m) \neq \zero$.
+    \begin{subproof}
+        Omitted.
+    \end{subproof}
+
+    We show that for all $m \in \naturals$ we have $\pot(m) \in \naturals$.
+    \begin{subproof}
+        Omitted.
+    \end{subproof}
+
+    
+%    We show that for all $m \in \indexxset[\zeta]$ we have there exist $f$ such that $f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$ 
+%    and for all $n \in \indexxset[\indexx[\zeta](m)]$ we have for all $x \in \indexx[\indexx[\zeta](m)](n)$ such that $x \notin \indexx[\indexx[\zeta](m)](n-1)$ 
+%    we have $f(x) = \rfrac{n}{\pot(m)}$.
+%    \begin{subproof}
+%        Fix $m \in \indexxset[\zeta]$.
+%        %$\indexx[\zeta](m)$ is a urysohnchain in $X$.
+%
+%        %Define $o : \alpha \to \intervalclosed{\zero}{1}$ such that $o(x) =$
+%        %\begin{cases}
+%        %    & 0  & \text{if} x \in A 
+%        %    & 1 & \text{if} x \in B 
+%        %    & \rfrac{n}{m} & \text{if} \exists n \in \naturals. x \in \indexx[\indexx[\zeta](m)](n) \land x \notin \indexx[\indexx[\zeta](m)](n-1)
+%        %\end{cases}
+%%
+%        Omitted.
+%    \end{subproof}
+%
+%    
+%
+%    %The sequenc of the functions
+%    Let $\gamma = \{
+%        (n,f) \mid 
+%        n \in \naturals \mid 
+%        
+%        \forall n' \in \indexxset[\indexx[\zeta](n)].             
+%        \forall x \in \carrier[X].      
+%        
+%
+%        f \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}} \land
+%
+%
+%        % (n,f) \in \gamma  <=>   \phi(n,f)
+%        % with \phi (n,f) :=        
+%        %    (x \in (A_k) \ (A_k-1)) ==> f(x) = ( k / 2^n )        
+%        % \/ (x \notin A_k for all k \in {1,..,n} ==>  f(x) = 1 
+%
+%            (       (n' = \zero)   
+%            \land   (x \in \indexx[\indexx[\zeta](n)](n')) 
+%            \land   (f(x)= \zero) ) 
+%        
+%        \lor
+%        
+%            (       (n' > \zero)    
+%            \land   (x \in \indexx[\indexx[\zeta](n)](n'))
+%            \land   (x \notin \indexx[\indexx[\zeta](n)](n'-1))
+%            \land   (f(x) = \rfrac{n'}{\pot(n)}) )
+%            
+%        \lor
+%
+%            (       (x \notin  \indexx[\indexx[\zeta](n)](n'))
+%            \land   (f(x) = 1) )
+%        
+%    \}$.
+%    
+%    Let $\gamma(n) = \apply{\gamma}{n}$ for $n \in \naturals$.
+%
+%    We show that for all $n \in \naturals$ we have $\gamma(n)$ 
+%    is a function from $\carrier[X]$ to $\reals$.
+%    \begin{subproof}
+%        Omitted.
+%    \end{subproof}
+%
+%    
+%    We show that for all $n \in \naturals$ we have $\gamma(n)$ 
+%    is a function from $\carrier[X]$ to $\intervalclosed{\zero}{1}$.
+%    \begin{subproof}
+%        Omitted.
+%    \end{subproof}
+%
+%    We show that $\gamma$ is a function from $\naturals$ to $\reals$.
+%    \begin{subproof}
+%        Omitted.
+%    \end{subproof}
+%
+%    We show that  for all $x,k,n$ such that $n\in \naturals$ and $k \in \naturals$ and $x \in \indexx[\indexx[\zeta](n)](k)$ we have $\apply{\gamma(n)}{x} =  \rfrac{k}{\pot(n)}$.
+%    \begin{subproof}
+%        Omitted.
+%    \end{subproof}
+%
+%    We show that for all $n \in \naturals$ for all $x \in \carrier[X]$ we have $\apply{\gamma(n)}{x} \in \intervalclosed{\zero}{1}$. 
+%    \begin{subproof}
+%        Fix $n \in \naturals$.
+%        Fix $x \in \carrier[X]$.
+%        Omitted.
+%    \end{subproof}
+%
+%
+%
+%    We show that 
+%    if $h$ is a function from $\naturals$ to $\reals$ and for all $n \in \naturals$ we have $h(n) \leq h(n+1)$ and there exist $B \in \reals$ such that $h(n) < B$ 
+%    then there exist $k \in \reals$ such that for all $m \in \naturals$ we have $h(m) \leq k$ and for all $k' \in \reals$ such that $k' < k$ we have there exist $M \in \naturals$ such that $k' < h(M)$.
+%    \begin{subproof}
+%        Omitted.
+%    \end{subproof} 
+%
+%
+%
+%    We show that there exist $g$ such that for all $x \in \carrier[X]$ we have there exist $k \in \reals$ such that  $g(x)= k$ and for all $\epsilon \in \reals$ such that $\epsilon > \zero$ we have there exist $N \in \naturals$ such that for all $N' \in \naturals$ such that $N' > N$ we have $\abs{\apply{\gamma(N')}{x} - k} < \epsilon$.
+%    \begin{subproof}       
+%        We show that for all $x \in \carrier[X]$ we have there exist $k \in \reals$ such that for all $\epsilon \in \reals$ such that $\epsilon > \zero$ we have there exist $N \in \naturals$ such that for all $N' \in \naturals$ such that $N' > N$ we have $\abs{\apply{\gamma(N')}{x} - k} < \epsilon$.
+%        \begin{subproof}
+%            Fix $x \in \carrier[X]$.
+%            
+%            Omitted.
+%            
+%            % Contradiction by \cref{two_in_naturals,function_apply_default,reals_axiom_zero_in_reals,dom_emptyset,notin_emptyset,funs_type_apply,neg,minus,abs_behavior1}.
+%            %Follows by \cref{two_in_naturals,function_apply_default,reals_axiom_zero_in_reals,dom_emptyset,notin_emptyset,funs_type_apply,neg,minus,abs_behavior1}.
+%        \end{subproof}
+%        Omitted.
+%    \end{subproof}
+%    
+%
+%    Let $G(x) = g(x)$ for $x \in \carrier[X]$.
+%    We have $\dom{G} = \carrier[X]$.
+%
+%    We show that for all $x \in \dom{G}$ we have $G(x) \in \reals$.
+%    \begin{subproof}
+%        %Fix $x \in \dom{G}$.
+%        %It suffices to show that $g(x) \in \reals$.
+%%
+%        %There exist $k \in \reals$ such that for all $\epsilon \in \reals$ such that $\epsilon > \zero$ we have there exist $N \in \naturals$ such that for all $N' \in \naturals$ such that $N' > N$ we have $\abs{\apply{\gamma(N')}{x} - k} < \epsilon$.
+%%
+%        %We show that for all $\epsilon \in \reals$ such that $\epsilon > \zero$ we have there exist $N \in \naturals$ such that for all $N' \in \naturals$ such that $N' > N$ we have $\abs{\apply{\gamma(N')}{x} - g(x)} < \epsilon$ and $g(x)= k$.
+%        %\begin{subproof}
+%        %    Fix $\epsilon \in \reals$.
+%        %    
+%%
+%        %\end{subproof}
+%        %Follows by \cref{apply,plus_one_order,ordinal_iff_suc_ordinal,natural_number_is_ordinal,subseteq,naturals_subseteq_reals,naturals_is_equal_to_two_times_naturals,reals_one_bigger_zero,one_in_reals,ordinal_prec_trichotomy,omega_is_an_ordinal,suc_intro_self,two_in_naturals,in_asymmetric,suc}.
+%        Omitted.
+%    \end{subproof}
+%
+%    We show that for all $x \in \dom{G}$ we have $\zero \leq G(x) \leq 1$.
+%    \begin{subproof}
+%        %Fix $x \in \dom{G}$.
+%        %Then $x \in \carrier[X]$.
+%        %\begin{byCase}
+%        %    \caseOf{$x \in A$.} 
+%        %        For all $n \in \naturals$ we have $\apply{\gamma(n)}{x} = \zero$.
+%%
+%%
+%        %    \caseOf{$x \notin A$.} 
+%        %        \begin{byCase}
+%        %            \caseOf{$x \in B$.} 
+%        %                For all $n \in \naturals$ we have $\apply{\gamma(n)}{x} = 1$.
+%%
+%        %            \caseOf{$x \notin B$.}
+%        %                Omitted.
+%        %        \end{byCase}
+%        %\end{byCase}
+%        Omitted.
+%    \end{subproof}
+%
+%
+%    We show that $G \in \funs{\carrier[X]}{\intervalclosed{\zero}{1}}$.
+%    \begin{subproof}        
+%        %It suffices to show that $\ran{G} \subseteq \intervalclosed{\zero}{1}$ by \cref{fun_ran_iff,funs_intro,funs_weaken_codom}.
+%        %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]$.
+%        %$g(x) = G(x)$.
+%        %We have $G(x) \in \reals$.
+%        %$\zero \leq G(x) \leq 1$.
+%        %We have $G(x) \in \intervalclosed{\zero}{1}$ .
+%        Omitted.
+%    \end{subproof}
+%
+%    We show that $G(A) = \zero$.
+%    \begin{subproof}
+%        Omitted.
+%    \end{subproof}
+%
+%    We show that $G(B) = 1$.
+%    \begin{subproof}
+%        Omitted.
+%    \end{subproof}
+%
+%    We show that $G$ is continuous.
+%    \begin{subproof}
+%        Omitted.
+%    \end{subproof}
+%
+%    %Suppose $\eta$ is a urysohnchain in $X$.
+%    %Suppose $\carrier[\eta] =\{A, (X \setminus B)\}$
+%    %and $\indexxset[\eta] = \{\zero, 1\}$
+%    %and $\indexx[\eta](\zero) = A$ 
+%    %and $\indexx[\eta](1) = (X \setminus B)$.
+%
+%
+%    %Then $\eta$ is a urysohnchain in $X$.
+%
+%    %   Take $P$ such that $P$ is a infinite sequence and $\indexxset[P] = \naturals$ and for all $i \in \indexxset[P]$ we have $\indexx[P](i) = \pow{X}$.
+%    %   
+%    %   We show that there exist $\zeta$ such that $\zeta$ is a infinite sequence 
+%    %   and for all $i \in \indexxset[\zeta]$ we have 
+%    %   $\indexx[\zeta](i)$ is a urysohnchain in $X$ of cardinality $i$
+%    %   and $A \subseteq \indexx[\zeta](i)$
+%    %   and $\indexx[\zeta](i) \subseteq (X \setminus B)$
+%    %   and for all $j \in \indexxset[\zeta]$ such that 
+%    %   $j < i$ we have for all $x \in \indexx[\zeta](j)$ we have $x \in \indexx[\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{urysohnone_safe}
+%    Contradiction.     
+%\end{theorem}
diff --git a/library/topology/urysohn2.tex b/library/topology/urysohn2.tex
new file mode 100644
index 0000000..a1a3ba0
--- /dev/null
+++ b/library/topology/urysohn2.tex
@@ -0,0 +1,989 @@
+\import{topology/topological-space.tex}
+\import{topology/separation.tex}
+\import{topology/continuous.tex}
+\import{topology/basis.tex}
+\import{numbers.tex}
+\import{function.tex}
+\import{set.tex}
+\import{cardinal.tex}
+\import{relation.tex}
+\import{relation/uniqueness.tex}
+\import{set/cons.tex}
+\import{set/powerset.tex}
+\import{set/fixpoint.tex}
+\import{set/product.tex}
+\import{topology/real-topological-space.tex}
+\import{set/equinumerosity.tex}
+
+\section{Urysohns Lemma}\label{form_sec_urysohn}
+
+
+
+
+\begin{definition}\label{sequence}
+    $X$ is a sequence iff $X$ is a function and $\dom{X} \subseteq \naturals$.
+\end{definition}
+
+
+\begin{abbreviation}\label{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$
+    we have there exist $A',B' \in \opens[X]$
+    such that  $A \subseteq A'$ and $B \subseteq B'$ and $A' \inter B' = \emptyset$.    
+\end{abbreviation}
+
+
+\begin{abbreviation}\label{at}
+    $\at{f}{n} = f(n)$.
+\end{abbreviation}
+
+
+\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 $n < m$ we have $\at{X}{n} \subseteq \at{X}{m}$. 
+\end{definition}
+
+
+\begin{definition}\label{urysohnchain}%<-- zulässig
+    $X$ is a urysohnchain of $Y$ iff $X$ is a chain of subsets in $Y$ and for all $n,m \in \dom{X}$ such that $n < m$ we have $\closure{\at{X}{n}}{Y} \subseteq \interior{\at{X}{m}}{Y}$.
+\end{definition}
+
+\begin{definition}\label{urysohn_finer_set}
+    $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 
+    $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}
+    $y$ follows $x$ in $I$ iff $x < y$ and $x,y \in I$ and for all $i \in I$ such that $x < i$ we have $y \leq i$.
+\end{definition}
+
+\begin{definition}\label{finer_smallest_step}
+    $Y$ is a minimal finer extention of $X$ in $U$ iff $Y$ is finer then $X$ in $U$ and for all $x_1,x_2 \in \dom{X}$ such that $x_1$ follows $x_2$ in $\dom{X}$ we have there exist $y \in \dom{Y}$ such that $y$ follows $x_1$ in $\dom{X}$ and $x_2$ follows $y$ in $\dom{X}$.
+\end{definition}
+
+\begin{definition}\label{sequence_of_reals}
+    $X$ is a sequence of reals iff $\ran{X} \subseteq \reals$.
+\end{definition}
+
+
+\begin{definition}\label{pointwise_convergence}
+    $X$ converge to $x$ iff for all $\epsilon \in \realsplus$ there exist $N \in \dom{X}$ such that for all $n \in \dom{X}$ such that $n > N$ we have $\at{X}{n} \in \epsBall{x}{\epsilon}$.
+\end{definition}
+
+
+\begin{proposition}\label{iff_sequence}
+    Suppose $X$ is a function.
+    Suppose $\dom{X} \subseteq \naturals$.
+    Then $X$ is a sequence.
+\end{proposition}
+
+\begin{definition}\label{lifted_urysohn_chain}
+    $U$ is a lifted urysohnchain of $X$ iff $U$ is a sequence and $\dom{U} = \naturals$ and for all $n \in \dom{U}$ we have $\at{U}{n}$ is a urysohnchain of $X$ and $\at{U}{\suc{n}}$ is a minimal finer extention of $\at{U}{n}$ in $X$.
+\end{definition}
+
+\begin{definition}\label{normal_ordered_urysohnchain}
+    $U$ is normal ordered iff there exist $n \in \naturals$ such that $\dom{U} = \seq{\zero}{n}$.
+\end{definition}
+
+\begin{definition}\label{bijection_of_urysohnchains}
+    $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}
+\begin{proof}
+    Follows by \cref{nat_is_transitiveset}.
+\end{proof}
+
+\begin{proposition}\label{naturals_elem_in_transitive}
+    If $n \in \naturals$ then $n$ is \in-transitive and every element of $n$ is \in-transitive. 
+    %If $n$ is a natural number then $n$ is \in-transitive and every element of $n$ is \in-transitive. 
+\end{proposition}
+
+\begin{proposition}\label{natural_number_is_ordinal_for_all}
+    For all $n \in \naturals$ we have $n$ is a ordinal.
+\end{proposition}
+
+\begin{proposition}\label{zero_is_in_minimal}
+    $\zero$ is an \in-minimal element of $\naturals$.
+\end{proposition}
+
+\begin{proposition}\label{natural_rless_eq_precedes}
+    For all $n,m \in \naturals$ we have $n \precedes m$ iff $n \in m$.
+\end{proposition}
+
+\begin{proposition}\label{naturals_precedes_suc}
+    For all $n \in \naturals$ we have $n \precedes \suc{n}$.
+\end{proposition}
+
+\begin{proposition}\label{zero_is_empty}
+    There exists no $x$ such that $x \in \zero$.
+\end{proposition}
+\begin{proof}
+    Follows by \cref{notin_emptyset}.
+\end{proof}
+
+\begin{proposition}\label{one_is_positiv}
+    $1$ is positiv.
+\end{proposition}
+
+\begin{proposition}\label{suc_of_positive_is_positive}
+    For all $n \in \naturals$ such that $n$ is positiv we have $\suc{n}$ is positiv.
+\end{proposition}
+
+\begin{proposition}\label{naturals_are_positiv_besides_zero}
+    For all $n \in \naturals$ such that $n \neq \zero$ we have $n$ is positiv.
+\end{proposition}
+\begin{proof}[Proof by \in-induction on $n$]
+    Assume $n \in \naturals$.
+    \begin{byCase}
+        \caseOf{$n = \zero$.} Trivial.
+        \caseOf{$n \neq \zero$.}
+            Take $k \in \naturals$ such that $\suc{k} = n$.
+    \end{byCase}
+\end{proof}
+
+
+
+\begin{proposition}\label{naturals_sum_eq_zero}
+    For all $n,m \in \naturals$ we have if $n+m = \zero$ then $n = m = \zero$.
+\end{proposition}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+\begin{proposition}\label{no_natural_between_n_and_suc_n}
+    For all $n,m \in \naturals$ we have not $n < m < \suc{n}$.
+\end{proposition}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+\begin{proposition}\label{naturals_is_zero_one_or_greater}
+    $\naturals = \{n \in \naturals \mid n > 1 \lor n = 1 \lor n = \zero\}$.
+\end{proposition}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+\begin{proposition}\label{naturals_one_zero_or_greater}
+    For all $l \in \naturals$ we have if $l < 1$ then $l = \zero$.
+\end{proposition}
+\begin{proof}
+    Follows by \cref{reals_order,naturals_subseteq_reals,subseteq,one_in_reals,naturals_is_zero_one_or_greater}.
+\end{proof}
+
+\begin{proposition}\label{naturals_rless_existence_of_lesser_natural}
+    For all $n \in \naturals$ we have for all $m \in \naturals$ such that $m < n$ there exist $k \in \naturals$ such that $m + k = n$.
+\end{proposition}
+\begin{proof}[Proof by \in-induction on $n$]
+    Assume $n \in \naturals$.
+    
+    \begin{byCase}
+        \caseOf{$n = \zero$.} 
+            
+            We show that for all $m \in \naturals$ such that $m < n$ we have there exist $k \in \naturals$ such that $m + k = n$.
+            \begin{subproof}[Proof by \in-induction on $m$]
+                Assume $m \in \naturals$.
+                \begin{byCase}
+                    \caseOf{$m = \zero$.}
+                        Trivial.
+                    \caseOf{$m \neq \zero$.}
+                        Trivial.
+                \end{byCase}
+            \end{subproof}
+        \caseOf{$n = 1$.}
+            Fix $m$.
+            For all $l \in \naturals$ we have if $l < 1$ then $l = \zero$.
+            Then $\zero + 1 = 1$.
+        \caseOf{$n > 1$.} 
+            Take $l \in \naturals$ such that $\suc{l} = n$.
+            Omitted.
+    \end{byCase}
+\end{proof}
+
+
+\begin{proposition}\label{rless_eq_in_for_naturals}
+    For all $n,m \in \naturals$ such that $n < m$ we have $n \in m$. 
+\end{proposition}
+\begin{proof}
+    We show that for all $n \in \naturals$ we have for all $m \in \naturals$ such that $m < n$ we have $m \in n$.
+    \begin{subproof}[Proof by \in-induction on $n$]
+        Assume $n \in \naturals$.
+        We show that for all $m \in \naturals$ such that$m < n$ we have $m \in n$.
+        \begin{subproof}[Proof by \in-induction on $m$]
+            Assume $m \in \naturals$.
+            \begin{byCase}
+                \caseOf{$\suc{m}=n$.}
+                \caseOf{$\suc{m}\neq n$.}  
+                      \begin{byCase}
+                        \caseOf{$n = \zero$.}
+                        \caseOf{$n \neq \zero$.}
+                            Take $l \in \naturals$ such that $\suc{l} = n$.
+                            Omitted.
+
+                      \end{byCase}
+            \end{byCase}
+        \end{subproof}
+    \end{subproof}
+    
+    %Fix $n \in \naturals$.
+
+    %\begin{byCase}
+    %    \caseOf{$n = \zero$.}
+    %        For all $k \in \naturals$ we have $k = \zero$ or $\zero < k$.
+    %        
+    %    \caseOf{$n \neq \zero$.}
+    %        Fix $m \in \naturals$.
+    %        It suffices to show that $m \in n$.
+    %\end{byCase}
+    
+\end{proof}
+
+
+
+\begin{proposition}\label{naturals_leq}
+    For all $n \in \naturals$ we have $\zero \leq n$.
+\end{proposition}
+
+
+
+
+\begin{proposition}\label{naturals_leq_on_suc}
+    For all $n,m \in \naturals$ such that $m < \suc{n}$ we have $m \leq n$.
+\end{proposition}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+\begin{proposition}\label{x_in_seq_iff}
+    Suppose $n,m,x \in \naturals$.
+    $x \in \seq{n}{m}$ iff $n \leq x \leq m$.
+\end{proposition}
+
+\begin{proposition}\label{seq_zero_to_n_eq_to_suc_n}
+    For all $n \in \naturals$ we have $\seq{\zero}{n} = \suc{n}$.
+\end{proposition}
+\begin{proof} [Proof by \in-induction on $n$]
+    Assume $n \in \naturals$.
+    $n \in \naturals$.
+    For all $m \in n$ we have $m \in \naturals$.
+    \begin{byCase}
+        \caseOf{$n = \zero$.}
+            It suffices to show that $1 = \seq{\zero}{\zero}$.
+            Follows by set extensionality.
+        \caseOf{$n \neq \zero$.}
+            Take $k$ such that $k \in \naturals$ and $\suc{k} = n$.
+            Then $k \in n$.
+            Therefore $\seq{\zero}{k} = \suc{k}$.
+            We show that $\seq{\zero}{n} = \seq{\zero}{k} \union \{n\}$.
+            \begin{subproof}
+                We show that $\seq{\zero}{n} \subseteq \seq{\zero}{k} \union \{n\}$.
+                \begin{subproof}
+                    It suffices to show that for all $x \in \seq{\zero}{n}$ we have $x \in \seq{\zero}{k} \union \{n\}$.
+                    $n \in \naturals$.
+                    $\zero \leq n$.
+                    $n \leq n$.
+                    We have $n \in \seq{\zero}{n}$.
+                    Therefore $\seq{\zero}{n}$ is inhabited.
+                    Take $x$ such that $x \in \seq{\zero}{n}$.
+                    Therefore $\zero \leq x \leq n$.
+                    $x = n$ or $x < n$.
+                    Then either $x = n$ or $x \leq k$.
+                    Therefore $x \in \seq{\zero}{k}$ or $x = n$.
+                    Follows by \cref{reals_order,natural_number_is_ordinal,ordinal_empty_or_emptyset_elem,naturals_leq_on_suc,reals_axiom_zero_in_reals,naturals_subseteq_reals,subseteq,union_intro_left,naturals_inductive_set,m_to_n_set,x_in_seq_iff,union_intro_right,singleton_intro}.
+                \end{subproof}
+                We show that $\seq{\zero}{k} \union \{n\} \subseteq \seq{\zero}{n}$.
+                \begin{subproof}
+                    It suffices to show that for all $x \in \seq{\zero}{k} \union \{n\}$ we have $x \in \seq{\zero}{n}$.
+                    $k \leq n$ by \cref{naturals_subseteq_reals,suc_eq_plus_one,plus_one_order,subseteq}.
+                    $k \in n$.
+                    $\seq{\zero}{k} = \suc{k}$ by assumption.            
+                    $n \in \naturals$.
+                    $\zero \leq n$.
+                    $n \leq n$.
+                    We have $n \in \seq{\zero}{n}$.
+                    Therefore $\seq{\zero}{n}$ is inhabited.
+                    Take $x$ such that $x \in \seq{\zero}{n}$.
+                    Therefore $\zero \leq x \leq n$.
+                    $x = n$ or $x < n$.
+                    Then either $x = n$ or $x \leq k$.
+                    Therefore $x \in \seq{\zero}{k}$ or $x = n$.
+                    Fix $x$.
+                    \begin{byCase}
+                        \caseOf{$x \in \seq{\zero}{k}$.}
+                            Trivial.
+                        \caseOf{$x = n$.}
+                            It suffices to show that $n \in \seq{\zero}{n}$.
+                    \end{byCase}
+                \end{subproof}
+                Trivial.
+            \end{subproof}
+            We have $\suc{n} = n \union \{n\}$.
+    \end{byCase}
+
+    %Assume $n$ is a natural number.
+    %We show that $\seq{\zero}{\zero}$ has cardinality $1$.
+    %\begin{subproof}
+    %    It suffices to show that $1 = \seq{\zero}{\zero}$.
+    %    Follows by set extensionality.
+    %\end{subproof}
+    %It suffices to show that if $n \neq \zero$ then $\seq{\zero}{n}$ has cardinality $\suc{n}$.
+    %We show that for all $m \in \naturals$ such that $m \neq \zero$ we have $\seq{\zero}{m}$ has cardinality $\suc{m}$.
+    %\begin{subproof}
+    %    Fix $m \in \naturals$.
+    %    Take $k$ such that $k \in \naturals$ and $\suc{k} = m$.
+    %    Then $k \in m$.
+    %\end{subproof}
+    
+    
+    %For all $n \in \naturals$ we have either $n = \zero$ or there exist $m \in \naturals$ such that $n = \suc{m}$.
+    %For all $n \in \naturals$ we have either $n = \zero$ or $\zero \in n$.
+    %We show that if $\seq{\zero}{n}$ has cardinality $\suc{n}$ then $\seq{\zero}{\suc{n}}$ has cardinality $\suc{\suc{n}}$.
+    %\begin{subproof}
+    %    Omitted.
+    %\end{subproof}
+\end{proof}
+
+\begin{proposition}\label{seq_zero_to_n_isomorph_to_suc_n}
+    For all $n \in \naturals$ we have $\seq{\zero}{n}$ has cardinality $\suc{n}$.
+\end{proposition}
+
+\begin{proposition}\label{bijection_naturals_order}
+    For all $M \subseteq \naturals$ such that $M$ is inhabited we have there exist $f,k$ such that $f$ is a bijection from $\seq{\zero}{k}$ to $M$ and $M$ has cardinality $\suc{k}$ and for all $n,m \in \seq{\zero}{k}$ such that $n < m$ we have $f(n) < f(m)$.
+\end{proposition}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+\begin{lemma}\label{naturals_suc_injective}
+    Suppose $n,m \in \naturals$.
+    $n = m$ iff $\suc{n} = \suc{m}$.
+\end{lemma}
+
+\begin{lemma}\label{naturals_rless_implies_not_eq}
+    Suppose $n,m \in \naturals$.
+    Suppose $n < m$.
+    Then $n \neq m$.
+\end{lemma}
+
+\begin{lemma}\label{cardinality_of_singleton}
+    For all $x$ such that $x \neq \emptyset$ we have $\{x\}$ has cardinality $1$.
+\end{lemma}
+\begin{proof}
+    Omitted.
+    %Fix $x$.
+    %Suppose $x \neq \emptyset$.
+    %Let $X = \{x\}$.
+    %$\seq{\zero}{\zero}=1$.
+    %$\seq{\zero}{\zero}$ has cardinality $1$.
+    %$X \setminus \{x\} = \emptyset$.
+    %$1 = \{\emptyset\}$.
+    %Let $F = \{(x,\emptyset)\}$.
+    %$F$ is a relation.
+    %$\dom{F} = X$.
+    %$\emptyset \in \ran{F}$.
+    %for all $x \in 1$ we have $x = \emptyset$.
+    %$\ran{F} = 1$.
+    %$F$ is injective.
+    %$F \in \surj{X}{1}$.
+    %$F$ is a bijection from $X$ to $1$.
+\end{proof}
+
+\begin{lemma}\label{cardinality_n_plus_1}
+    For all $n \in \naturals$ we have $n+1$ has cardinality $n+1$.
+\end{lemma}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+\begin{lemma}\label{cardinality_n_m_plus}
+    For all $n,m \in \naturals$ we have $n+m$ has cardinality $n+m$.
+\end{lemma}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+\begin{lemma}\label{cardinality_plus_disjoint}
+    Suppose $X \inter Y = \emptyset$.
+    Suppose $X$ is finite.
+    Suppose $Y$ is finite.
+    Suppose $X$ has cardinality $n$.
+    Suppose $Y$ has cardinality $m$.
+    Then $X \union Y$ has cardinality $m+n$.
+\end{lemma}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+
+
+
+\begin{lemma}\label{injective_functions_is_bijection_if_bijection_there_is_other_bijection_1}
+    Suppose $f$ is a bijection from $X$ to $Y$.
+    Suppose $g$ is a function from $X$ to $Y$.
+    Suppose $g$ is injective.
+    Suppose $X$ is finite and $Y$ is finite. 
+    For all $n \in \naturals$ such that $Y$ has cardinality $n$ we have $g$ is a bijection from $X$ to $Y$.
+\end{lemma}
+\begin{proof}[Proof by \in-induction on $n$]
+    Assume $n \in \naturals$.
+    Suppose $Y$ has cardinality $n$.
+    $X$ has cardinality $n$ by \cref{bijection_converse_is_bijection,bijection_circ,regularity,cardinality,foundation,empty_eq,notin_emptyset}.
+    \begin{byCase}
+        \caseOf{$n = \zero$.} 
+            Follows by \cref{converse_converse_eq,injective_converse_is_function,converse_is_relation,dom_converse,id_is_function_to,id_ran,ran_circ_exact,circ,ran_converse,emptyset_is_function_on_emptyset,bijective_converse_are_funs,relext,function_member_elim,bijection_is_function,cardinality,bijections_dom,in_irrefl,codom_of_emptyset_can_be_anything,converse_emptyset,funs_elim,neq_witness,id}.
+        \caseOf{$n \neq \zero$.}
+            %Take $n' \in n$ such that $n = \suc{n'}$.
+            %$n' \in \naturals$.
+            %$n' + 1 = n$.
+            %Take $y$ such that $y \in Y$ by \cref{funs_type_apply,apply,bijections_to_funs,cardinality,foundation}. 
+            %Let $Y' = Y \setminus \{y\}$.
+            %$Y' \subseteq Y$.
+            %$Y'$ is finite.
+            %There exist $m \in \naturals$ such that $Y'$ has cardinality $m$.
+            %Take $m \in \naturals$ such that $Y'$ has cardinality $m$.
+            %Then $Y'$ has cardinality $n'$.
+            %Let $x' = \apply{\converse{f}}{y'}$. 
+            %$x' \in X$.
+            %Let $X' = X \setminus \{x'\}$.
+            %$X' \subseteq X$.
+            %$X'$ is finite.
+            %There exist $m' \in \naturals$ such that $X'$ has cardinality $m'$.
+            %Take $m' \in \naturals$ such that $X''$ has cardinality $m'$.
+            %Then $X'$ has cardinality $n'$.
+            %Let $f'(z)=f(z)$ for $z \in X'$.
+            %$\dom{f'} = X'$.
+            %$\ran{f'} = Y'$.
+            %$f'$ is a bijection from $X'$ to $Y'$.
+            %Let $g'(z) = g(z)$ for $z \in X'$.
+            %Then $g'$ is injective.
+            %Then $g'$ is a bijection from $X'$ to $Y'$ by \cref{rels,id_elem_rels,times_empty_right,powerset_emptyset,double_complement_union,unions_cons,union_eq_cons,union_as_unions,unions_pow,cons_absorb,setminus_self,bijections_dom,ran_converse,id_apply,apply,unions_emptyset,img_emptyset,zero_is_empty}.
+            %Define $G : X \to Y$ such that $G(z)=
+            %\begin{cases}
+            %    g'(z) & \text{if} z \in X' \\
+            %    y' & \text{if} z = x'
+            %\end{cases}$
+            %$G = g$.
+            %Follows by \cref{double_relative_complement,fun_to_surj,bijections,funs_surj_iff,bijections_to_funs,neq_witness,surj,funs_elim,setminus_self,cons_subseteq_iff,cardinality,ordinal_empty_or_emptyset_elem,naturals_inductive_set,natural_number_is_ordinal_for_all,foundation,inter_eq_left_implies_subseteq,inter_emptyset,cons_subseteq_intro,emptyset_subseteq}.
+            Omitted.
+    \end{byCase}
+    %$\converse{f}$ is a bijection from $Y$ to $X$.
+    %Let $h = g \circ \converse{f}$.
+    %It suffices to show that $\ran{g} = Y$ by \cref{fun_to_surj,dom_converse,bijections}.
+    %It suffices to show that for all $y \in Y$ we have there exist $x \in X$ such that $g(x)=y$ by \cref{funs_ran,subseteq_antisymmetric,fun_ran_iff,apply,funs_elim,ran_converse,subseteq}.
+%
+    %Fix $y \in Y$.
+    %Take $x \in X$ such that $\apply{\converse{f}}{y} = x$.
+
+\end{proof}
+
+\begin{lemma}\label{injective_functions_is_bijection_if_bijection_there_is_other_bijection}
+    Suppose $f$ is a bijection from $X$ to $Y$.
+    Suppose $g$ is a function from $X$ to $Y$.
+    Suppose $g$ is injective.
+    Suppose $Y$ is finite. 
+    Then $g$ is a bijection from $X$ to $Y$.
+\end{lemma}
+\begin{proof}
+    There exist $n \in \naturals$ such that $Y$ has cardinality $n$ by \cref{cardinality,injective_functions_is_bijection_if_bijection_there_is_other_bijection_1,finite}.
+    Follows by \cref{injective_functions_is_bijection_if_bijection_there_is_other_bijection_1,cardinality,equinum_tran,equinum_sym,equinum,finite}.
+\end{proof}
+
+
+
+\begin{lemma}\label{naturals_bijection_implies_eq}
+    Suppose $n,m \in \naturals$.
+    Suppose $f$ is a bijection from $n$ to $m$.
+    Then $n = m$.
+\end{lemma}
+\begin{proof}
+    $n$ is finite.
+    $m$ is finite.
+    Suppose not.
+    Then $n < m$ or $m < n$.
+    \begin{byCase}
+        \caseOf{$n < m$.}
+            Then $n \in m$.
+            There exist $x \in m$ such that $x \notin n$.
+            $\identity{n}$ is a function from $n$ to $m$.
+            $\identity{n}$ is injective.
+            $\apply{\identity{n}}{n} = n$ by \cref{id_ran,ran_of_surj,bijections,injective_functions_is_bijection_if_bijection_there_is_other_bijection}.
+            Follows by \cref{inhabited,regularity,function_apply_default,apply,id_dom,in_irrefl,function_member_elim,bijections_dom,zero_is_empty,bijection_is_function,foundation,bijections,ran_of_surj,dom_converse,converse_emptyset,dom_emptyset}.
+        \caseOf{$m < n$.}
+            Then $m \in n$.
+            There exist $x \in n$ such that $x \notin m$.
+            $\converse{f}$ is a bijection from $m$ to $n$.
+            $\identity{m}$ is a function from $m$ to $n$.
+            $\identity{m}$ is injective.
+            $\apply{\identity{m}}{m} = m$ by \cref{id_ran,ran_of_surj,bijections,injective_functions_is_bijection_if_bijection_there_is_other_bijection}.
+            Follows by \cref{inhabited,regularity,function_apply_default,apply,id_dom,in_irrefl,function_member_elim,bijections_dom,zero_is_empty,bijection_is_function,foundation,bijections,ran_of_surj,dom_converse,converse_emptyset,dom_emptyset}.
+    \end{byCase}
+\end{proof}
+
+\begin{lemma}\label{naturals_eq_iff_bijection}
+    Suppose $n,m \in \naturals$.
+    $n = m$ iff there exist $f$ such that $f$ is a bijection from $n$ to $m$.
+\end{lemma}
+\begin{proof}
+    We show that if $n = m$ then there exist $f$ such that $f$ is a bijection from $n$ to $m$.
+    \begin{subproof}
+        Trivial.
+    \end{subproof}
+    We show that for all $k \in \naturals$ we have if there exist $f$ such that $f$ is a bijection from $k$ to $m$ then $k = m$.
+    \begin{subproof}%[Proof by \in-induction on $k$]
+        %Assume $k \in \naturals$.
+        %\begin{byCase}
+        %    \caseOf{$k = \zero$.} 
+        %        Trivial.
+        %    \caseOf{$k \neq \zero$.}
+        %        \begin{byCase}
+        %            \caseOf{$m = \zero$.}
+        %                Trivial.
+        %            \caseOf{$m \neq \zero$.}
+        %                Take $k' \in \naturals$ such that $\suc{k'} = k$.
+        %                Then $k' \in k$.
+        %                Take $m' \in \naturals$ such that $m = \suc{m'}$.
+        %                Then $m' \in m$.
+        %                
+        %        \end{byCase}
+        %\end{byCase}
+    \end{subproof}
+\end{proof}
+
+\begin{lemma}\label{seq_from_zero_suc_cardinality_eq_upper_border}
+    Suppose $n,m \in \naturals$.
+    Suppose $\seq{\zero}{n}$ has cardinality $\suc{m}$.
+    Then $n = m$.
+\end{lemma}
+\begin{proof}
+    We have $\seq{\zero}{n} = \suc{n}$.
+    Take $f$ such that $f$ is a bijection from $\seq{\zero}{n}$ to $\suc{m}$.
+    Therefore $n=m$ by \cref{suc_injective,naturals_inductive_set,cardinality,naturals_eq_iff_bijection}.
+\end{proof}
+
+\begin{lemma}\label{seq_from_zero_cardinality_eq_upper_border_set_eq}
+    Suppose $n,m \in \naturals$.
+    Suppose $\seq{\zero}{n}$ has cardinality $\suc{m}$.
+    Then $\seq{\zero}{n} = \seq{\zero}{m}$.
+\end{lemma}
+
+\begin{proposition}\label{existence_normal_ordered_urysohn}
+    Let $X$ be a urysohn space.
+    Suppose $U$ is a urysohnchain of $X$.
+    Suppose $\dom{U}$ is finite.
+    Suppose $U$ is inhabited.
+    Then there exist $V,f$ such that $V$ is a urysohnchain of $X$ and $f$ is consistent on $V$ to $U$ and $V$ is normal ordered.
+\end{proposition}
+\begin{proof}
+    Take $n$ such that $\dom{U}$ has cardinality $n$ by \cref{ran_converse,cardinality,finite}.
+    \begin{byCase}
+        \caseOf{$n = \zero$.} 
+            Omitted.
+        \caseOf{$n \neq \zero$.}
+            Take $k$ such that $k \in \naturals$ and $\suc{k}=n$. 
+            We have $\dom{U} \subseteq \naturals$.
+            $\dom{U}$ is inhabited by \cref{downward_closure,downward_closure_iff,rightunique,function_member_elim,inhabited,chain_of_subsets,urysohnchain,sequence}.
+            $\dom{U}$ has cardinality $\suc{k}$.
+            We show that there exist $F$ such that $F$ is a bijection from $\seq{\zero}{k}$ to $\dom{U}$ and for all $n',m' \in \seq{\zero}{k}$ such that $n' < m'$ we have $F(n') < F(m')$.
+            \begin{subproof}
+                For all $M \subseteq \naturals$ such that $M$ is inhabited we have there exist $f,k$ such that $f$ is a bijection from $\seq{\zero}{k}$ to $M$ and $M$ has cardinality $\suc{k}$ and for all $n,m \in \seq{\zero}{k}$ such that $n < m$ we have $f(n) < f(m)$.
+                We have $\dom{U} \subseteq \naturals$.
+                $\dom{U}$ is inhabited.
+                Therefore there exist $f$ such that there exist $k'$ such that $f$ is a bijection from $\seq{\zero}{k'}$ to $\dom{U}$ and $\dom{U}$ has cardinality $\suc{k'}$ and for all $n',m' \in \seq{\zero}{k'}$ such that $n' < m'$ we have $f(n') < f(m')$.
+                Take $f$ such that there exist $k'$ such that $f$ is a bijection from $\seq{\zero}{k'}$ to $\dom{U}$ and $\dom{U}$ has cardinality $\suc{k'}$ and for all $n',m' \in \seq{\zero}{k'}$ such that $n' < m'$ we have $f(n') < f(m')$.
+                Take $k'$ such that $f$ is a bijection from $\seq{\zero}{k'}$ to $\dom{U}$ and $\dom{U}$ has cardinality $\suc{k'}$ and for all $n',m' \in \seq{\zero}{k'}$ such that $n' < m'$ we have $f(n') < f(m')$.
+                $\seq{\zero}{k'}$ has cardinality $\suc{k}$ by \cref{omega_is_an_ordinal,suc,ordinal_transitivity,bijection_converse_is_bijection,seq_zero_to_n_eq_to_suc_n,cardinality,bijections_dom,bijection_circ}.
+                $\seq{\zero}{k'} = \seq{\zero}{k}$ by \cref{omega_is_an_ordinal,seq_from_zero_cardinality_eq_upper_border_set_eq,suc_subseteq_implies_in,suc_subseteq_elim,ordinal_suc_subseteq,cardinality}.
+                %We show that $\seq{\zero}{k'} = \seq{\zero}{k}$.
+                %\begin{subproof}
+                %    We show that $\seq{\zero}{k'} \subseteq \seq{\zero}{k}$.
+                %    \begin{subproof}
+                %        It suffices to show that for all $y \in \seq{\zero}{k'}$ we have $y \in \seq{\zero}{k}$.
+                %        Fix $y \in \seq{\emptyset}{k'}$.
+                %        Then $y \leq k'$.
+                %        Therefore $y \in k'$ or $y = k'$ by \cref{omega_is_an_ordinal,suc_intro_self,ordinal_transitivity,cardinality,rless_eq_in_for_naturals,m_to_n_set}.
+                %        
+                %        Therefore $y \in \suc{k}$.
+                %        Therefore $y \in \seq{\emptyset}{k}$.
+                %    \end{subproof}
+                %    We show that for all $y \in \seq{\zero}{k}$ we have $y \in \seq{\zero}{k'}$.
+                %    \begin{subproof}
+                %        Fix $y \in \seq{\emptyset}{k}$.
+                %    \end{subproof}
+                %\end{subproof}
+            \end{subproof}
+            Take $F$ such that $F$ is a bijection from $\seq{\zero}{k}$ to $\dom{U}$ and for all $n',m' \in \seq{\zero}{k}$ such that $n' < m'$ we have $F(n') < F(m')$.
+            Let $N = \seq{\zero}{k}$.
+            Let $M = \pow{X}$.
+            Define $V : N \to M$ such that $V(n)=
+            \begin{cases}
+                \at{U}{F(n)} & \text{if} n \in N
+            \end{cases}$
+            $\dom{V} = \seq{\zero}{k}$.
+            We show that $V$ is a urysohnchain of $X$.
+            \begin{subproof}
+                It suffices to show that $V$ is a chain of subsets in $X$ and for all $n,m \in \dom{V}$ such that $n < m$ we have $\closure{\at{V}{n}}{X} \subseteq \interior{\at{V}{m}}{X}$.
+                We show that $V$ is a chain of subsets in $X$.
+                \begin{subproof}
+                    It suffices to show that $V$ is a sequence and for all $n \in \dom{V}$ we have $\at{V}{n} \subseteq \carrier[X]$ and for all $m \in \dom{V}$ such that $m > n$ we have $\at{V}{n} \subseteq \at{V}{m}$.
+                    $V$ is a sequence by \cref{m_to_n_set,sequence,subseteq}.
+                    It suffices to show that for all $n \in \dom{V}$ we have $\at{V}{n} \subseteq \carrier[X]$ and for all $m \in \dom{V}$ such that $m > n$ we have $\at{V}{n} \subseteq \at{V}{m}$.
+                    Fix $n \in \dom{V}$.
+                    Then $\at{V}{n} \subseteq \carrier[X]$ by \cref{ran_converse,seq_zero_to_n_eq_to_suc_n,in_irrefl}.
+                    It suffices to show that for all $m$ such that $m \in \dom{V}$ and $n \rless m$ we have $\at{V}{n} \subseteq \at{V}{m}$.
+                    Fix $m$ such that $m \in \dom{V}$ and $n \rless m$.
+                    Follows by \cref{ran_converse,seq_zero_to_n_eq_to_suc_n,in_irrefl}.
+                \end{subproof}
+                It suffices to show that for all $n \in \dom{V}$ we have for all $m$ such that $m \in \dom{V} \land n \rless m$ we have $\closure{\at{V}{n}}{X} \subseteq \interior{\at{V}{m}}{X}$.
+                Fix $n \in \dom{V}$.
+                Fix $m$ such that $m \in \dom{V} \land n \rless m$.
+                Follows by \cref{ran_converse,seq_zero_to_n_eq_to_suc_n,in_irrefl}.
+            \end{subproof}
+            We show that $F$ is consistent on $V$ to $U$.
+            \begin{subproof}
+                It suffices to show that $F$ is a bijection from $\dom{V}$ to $\dom{U}$ and for all $n,m \in \dom{V}$ such that $n < m$ we have $F(n) < F(m)$ by \cref{bijection_of_urysohnchains}.
+                $F$ is a bijection from $\dom{V}$ to $\dom{U}$.
+                It suffices to show that for all $n \in \dom{V}$ we have for all $m$ such that $m \in \dom{V}$ and $n \rless m$ we have $f(n) < f(m)$.
+                Fix $n \in \dom{V}$.
+                Fix $m$ such that $m \in \dom{V}$ and $n \rless m$.
+                Follows by \cref{ran_converse,seq_zero_to_n_eq_to_suc_n,in_irrefl}.
+            \end{subproof}
+            $V$ is normal ordered.
+    \end{byCase}
+    
+\end{proof}
+
+
+\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{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.
+    Suppose $A,B \in \closeds{X}$.
+    Suppose $\closure{A}{X} \subseteq \interior{B}{X}$.
+    Suppose $\carrier[X]$ is inhabited.
+    There exist $U \subseteq \carrier[X]$ such that $U$ is closed in $X$ and $\closure{A}{X} \subseteq \interior{U}{X} \subseteq \closure{U}{X} \subseteq \interior{B}{X}$.
+\end{theorem}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+
+\begin{theorem}\label{induction_on_urysohnchains}
+    Let $X$ be a urysohn space.
+    Suppose $U_0$ is a sequence.
+    Suppose $U_0$ is a chain of subsets in $X$.
+    Suppose $U_0$ is a urysohnchain of $X$.
+    There exist $U$ such that $U$ is a sequence and $\dom{U} = \naturals$ and $\at{U}{\zero} = U_0$ and for all $n \in \dom{U}$ we have $\at{U}{n}$ is a urysohnchain of $X$ and $\at{U}{\suc{n}}$ is a minimal finer extention of $\at{U}{n}$ in $X$.
+\end{theorem}
+\begin{proof}
+    %$U_0$ is a urysohnchain of $X$.
+    %It suffices to show that for all $V$ such that $V$ is a urysohnchain of $X$ there exist $V'$ such that $V'$ is a urysohnchain of $X$ and $V'$ is a minimal finer extention of $V$ in $X$.
+    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}
+    Let $X$ be a urysohn space.
+    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$ 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]$.
+    Let $N = \{\zero, 1\}$.
+    $1 = \suc{\zero}$.
+    $1 \in \naturals$ and $\zero \in \naturals$.
+    $N \subseteq \naturals$.
+    Let $A' = (X' \setminus B)$.
+    $B \subseteq X'$ by \cref{powerset_elim,closeds}.
+    $A \subseteq X'$.
+    Therefore $A \subseteq A'$.
+    Define $U_0: N \to \{A, A'\}$ such that $U_0(n) =
+    \begin{cases}
+        A  &\text{if} n = \zero \\
+        A' &\text{if} n = 1
+    \end{cases}$
+    $U_0$ is a function.
+    $\dom{U_0} = N$.
+    $\dom{U_0} \subseteq \naturals$ by \cref{ran_converse}. 
+    $U_0$ is a sequence.
+    We have $1, \zero \in N$.
+    We show that $U_0$ is a chain of subsets in $X$.
+    \begin{subproof}
+        We have $\dom{U_0} \subseteq \naturals$.
+        We have for all $n \in \dom{U_0}$ we have $\at{U_0}{n} \subseteq \carrier[X]$ by \cref{topological_prebasis_iff_covering_family,union_as_unions,union_absorb_subseteq_left,subset_transitive,setminus_subseteq}.
+        We have $\dom{U_0} = \{\zero, 1\}$.
+
+        It suffices to show that for all $n \in \dom{U_0}$ we have for all $m \in \dom{U_0}$ such that $m > n$ we have $\at{U_0}{n} \subseteq \at{U_0}{m}$.
+
+        Fix $n \in \dom{U_0}$.
+        Fix $m \in \dom{U_0}$.
+
+        \begin{byCase}
+            \caseOf{$n \neq \zero$.} 
+                Trivial.
+            \caseOf{$n = \zero$.} 
+                \begin{byCase}
+                    \caseOf{$m = \zero$.} 
+                        Trivial.
+                    \caseOf{$m \neq \zero$.}
+                        We have $A \subseteq A'$.
+                        We have $\at{U_0}{\zero} = A$ by assumption.
+                        We have $\at{U_0}{1}= A'$ by assumption.
+                        Follows by \cref{powerset_elim,emptyset_subseteq,union_as_unions,union_absorb_subseteq_left,subseteq_pow_unions,ran_converse,subseteq,subseteq_antisymmetric,suc_subseteq_intro,apply,powerset_emptyset,emptyset_is_ordinal,notin_emptyset,ordinal_elem_connex,omega_is_an_ordinal,prec_is_ordinal}.
+                \end{byCase}
+        \end{byCase}
+    \end{subproof}
+
+    We show that $U_0$ is a urysohnchain of $X$.
+    \begin{subproof}
+        It suffices to show that for all $n \in \dom{U_0}$ we have for all $m \in \dom{U_0}$ such that $n < m$ we have $\closure{\at{U_0}{n}}{X} \subseteq \interior{\at{U_0}{m}}{X}$.
+        Fix $n \in \dom{U_0}$.
+        Fix $m \in \dom{U_0}$.
+        \begin{byCase}
+            \caseOf{$n \neq \zero$.} 
+                Follows by \cref{ran_converse,upair_iff,one_in_reals,order_reals_lemma0,reals_axiom_zero_in_reals,reals_one_bigger_zero,reals_order}.
+            \caseOf{$n = \zero$.} 
+                \begin{byCase}
+                    \caseOf{$m = \zero$.} 
+                        Trivial.
+                    \caseOf{$m \neq \zero$.}
+                        Follows by \cref{setminus_emptyset,setdifference_eq_intersection_with_complement,setminus_self,interior_carrier,complement_interior_eq_closure_complement,subseteq_refl,closure_interior_frontier_is_in_carrier,emptyset_subseteq,closure_is_minimal_closed_set,inter_lower_right,inter_lower_left,subseteq_transitive,interior_of_open,is_closed_in,closeds,union_absorb_subseteq_right,ordinal_suc_subseteq,ordinal_empty_or_emptyset_elem,union_absorb_subseteq_left,union_emptyset,topological_prebasis_iff_covering_family,inhabited,notin_emptyset,subseteq,union_as_unions,natural_number_is_ordinal}.
+                \end{byCase}
+        \end{byCase}
+    \end{subproof}
+    %We are done with the first step, now we want to prove that we have U a sequence of these chain with U_0 the first chain.
+
+    We show that there exist $U$ such that $U$ is a sequence and $\dom{U} = \naturals$ and $\at{U}{\zero} = U_0$ and for all $n \in \dom{U}$ we have $\at{U}{n}$ is a urysohnchain of $X$ and $\at{U}{\suc{n}}$ is a minimal finer extention of $\at{U}{n}$ in $X$.
+    \begin{subproof}
+        Follows by \cref{chain_of_subsets,urysohnchain,induction_on_urysohnchains}.
+    \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$ in $X$.
+    \begin{subproof}
+        Omitted.
+    \end{subproof}
+    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}$.
+                    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})$.
+                    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}$.}
+                            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}
+
+            
+
+            %$\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}
+
+
+
+
+
+
diff --git a/library/wunschzettel.tex b/library/wunschzettel.tex
new file mode 100644
index 0000000..74ea899
--- /dev/null
+++ b/library/wunschzettel.tex
@@ -0,0 +1,108 @@
+%This is just a .tex file with a wishlist of functionalitys 
+
+
+Tupel struct
+
+\newtheorem{struct2}[theoremcount]{Struct2}
+
+\begin{theorem}
+    %Some Theorem.
+\end{theorem}
+\begin{proof}
+    %Wish for nice Function definition. --------------------- 
+
+    %Some Proof where we need a Function.
+    %Privisuly defined.
+    $n \in \naturals$.
+    There is a Set $A = \{A_{0}, ..., A_{n}\}$.
+    For all $i$ we have $A_{i} \subseteq X$.
+
+    Define function $f: X \to Y$,
+    \begin{align}
+        &x \mapsto \rfrac{y}{n} &; if \exists k \in \{1, ... n\}. x \in A_{k} \\
+        &x \mapsto 0 &; if x  \phi(x) \\ 
+        %phi is some fol formula
+
+        &x \mapsto \eta &; for \phi(x) and \psi(\eta) 
+
+        &x \mapsto \some_term(x)(u)(v)(w) &; \exist.u,v,w \psi(x)(u)(v)(w) \\ 
+        % here i see the real need of varibles that can be useds in the define term
+
+        &x \mapsto \some_else_term(x)   &; else 
+        % the else term would be great 
+
+        % the following axioms should be automaticly added.
+        % \dom{f} = X
+        % \ran{f} \subseteq Y
+        % f is function
+
+        % therefor we should add the prompt for a proof that f is well defined
+    \end{align}
+    \begin{proof_well_defined}
+        % we need to proof that f allways maps X to Y
+    \end{proof_well_defined}
+
+    % more proof but now i can use the function f
+
+    % --------------------------------------------------------
+    \begin{equation}
+        X=
+        \begin{cases}
+          0, & \text{if}\ a=1 \\
+          1, & \text{otherwise}
+        \end{cases}
+      \end{equation}
+
+
+
+
+\end{proof}
+
+
+%------------------------------------------
+% My wish for a new struct 
+% I think this could be just get implemented along with the old struct
+
+
+% If take we only take tupels,
+% then just a list of defining fol formulas should be enougth. 
+\begin{struct2}
+    We say $(X,O)$ is a topological space if
+    \begin{enumerate}
+        \item $X$ is a set. % or X = \{...\mid .. \} or X = \naturals ... or ...
+        \item $O \subseteq \pow X$.
+        \item $\forall x,y \in O. x \union y \in O$ 
+        \item %another formula
+        \item %....
+    \end{enumerate} 
+\end{struct2}
+
+
+% Then the proof of some thing is a structure is more easy.
+% Since if we have just a tupel and some formulas which has to be fufilled,
+% then we can make a proof as follows.
+
+\begin{struct2}
+    We say $(A,i,N)$ is a indexed set if
+    \begin{enumerate}
+        \item $f$ is a bijection from $N$ to $A$
+        \item $N \subseteq \naturals$
+    \end{enumerate}
+\end{struct2}
+
+
+\begin{theorem}
+    Let $A = \{ \{n\} \mid n \in \naturals \}$.
+    Let function $f: \naturals \to \pow{\naturals}$ such that,
+    \begin{algin}
+        \item x \mapsto \{x\} ; x \in \naturals
+    \end{algin}
+    Then $(A, f, \naturals)$ is a indexed set.
+\end{theorem}
+\begin{proof}
+    % Then we only need to proof that:
+    % \ran{f} = A
+    % \dom{f} = \naturals
+    % f is a bijection between $\naturals$ to $A$.
+\end{proof}
+
diff --git a/source/Api.hs b/source/Api.hs
index 95d5c8c..1bdf615 100644
--- a/source/Api.hs
+++ b/source/Api.hs
@@ -17,6 +17,7 @@ module Api
     , dumpTask
     , verify, ProverAnswer(..), VerificationResult(..)
     , exportMegalodon
+    , showFailedTask
     , WithCache(..)
     , WithFilter(..)
     , WithOmissions(..)
@@ -29,6 +30,7 @@ module Api
     , WithParseOnly(..)
     , Options(..)
     , WithDumpPremselTraining(..)
+    , WithFailList(..)
     ) where
 
 
@@ -65,6 +67,7 @@ import Text.Megaparsec hiding (parse, Token)
 import UnliftIO
 import UnliftIO.Directory
 import UnliftIO.Environment
+import Syntax.Abstract (Formula)
 
 -- | Follow all @\\import@ statements recursively and build a theory graph from them.
 -- The @\\import@ statements should be on their own separate line and precede all
@@ -200,7 +203,9 @@ describeToken = \case
     EndEnv _ -> "end of environment"
     _ -> "delimiter"
 
-
+-- | gloss generates internal represantation of the LaTeX files.
+-- First the file will be parsed and therefore checkt for grammer.
+-- 'meaning' then transfer the raw parsed grammer to the internal semantics.
 gloss :: MonadIO io => FilePath -> io ([Internal.Block], Lexicon)
 gloss file = do
     (blocks, lexicon) <- parse file
@@ -285,6 +290,17 @@ exportMegalodon file = do
     pure (Megalodon.encodeBlocks lexicon blocks)
 
 
+
+-- | This could be expandend with the dump case, with dump off just this and if dump is on it could show the number off the task. For quick use
+showFailedTask :: (a, ProverAnswer) -> IO()
+showFailedTask (_, Yes ) = Text.putStrLn ""
+showFailedTask (_, No tptp) = Text.putStrLn (Text.pack ("\ESC[31mProver found countermodel: \ESC[0m" ++ Text.unpack(Text.unlines (take 1 (Text.splitOn "." tptp)))))
+showFailedTask (_, ContradictoryAxioms tptp) = Text.putStrLn (Text.pack ("\ESC[31mContradictory axioms: \ESC[0m" ++ Text.unpack(Text.unlines (take 1 (Text.splitOn "." tptp)))))
+showFailedTask (_, Uncertain tptp) = Text.putStrLn (Text.pack ("\ESC[31mOut of resources: \ESC[0m" ++ Text.unpack(Text.unlines (take 1 (Text.splitOn "." tptp)))))
+showFailedTask (_, Error _ tptp _) = Text.putStrLn (Text.pack ("\ESC[31mError at: \ESC[0m" ++ Text.unpack(Text.unlines (take 1 (Text.splitOn "." tptp)))))
+--showFailedTask (_, _) = Text.putStrLn "Error!"
+
+
 -- | Should we use caching?
 data WithCache = WithoutCache | WithCache deriving (Show, Eq)
 
@@ -312,6 +328,8 @@ pattern WithoutDump = WithDump ""
 
 data WithParseOnly = WithoutParseOnly | WithParseOnly deriving (Show, Eq)
 
+data WithFailList = WithoutFailList | WithFailList deriving (Show, Eq)
+
 
 data Options = Options
     { inputPath :: FilePath
@@ -327,4 +345,5 @@ data Options = Options
     , withVersion :: WithVersion
     , withMegalodon :: WithMegalodon
     , withDumpPremselTraining :: WithDumpPremselTraining
+    , withFailList :: WithFailList
     }
diff --git a/source/Checking.hs b/source/Checking.hs
index dc90264..8bc38a4 100644
--- a/source/Checking.hs
+++ b/source/Checking.hs
@@ -28,6 +28,7 @@ import Data.HashSet qualified as HS
 import Data.InsOrdMap (InsOrdMap)
 import Data.InsOrdMap qualified as InsOrdMap
 import Data.List qualified as List
+import Data.List.NonEmpty qualified as NonEmpty
 import Data.Set qualified as Set
 import Data.Text qualified as Text
 import Data.Text.IO qualified as Text
@@ -149,7 +150,7 @@ assume asms = traverse_ go asms
         go :: Asm -> Checking
         go = \case
             Asm phi -> do
-                phi' <-  (canonicalize phi)
+                phi' <- canonicalize phi
                 modify \st ->
                     st{ checkingAssumptions = phi' : checkingAssumptions st
                     , fixedVars = freeVars phi' <> fixedVars st
@@ -542,6 +543,56 @@ checkProof = \case
         checkCalc calc
         assume [Asm (calcResult calc)]
         checkProof continue
+    DefineFunctionLocal funVar argVar domVar ranExpr definitions continue -> do
+        -- We have f: X \to Y and x \mapsto ...  
+        -- definition is a nonempty list of (expresssion e, formula phi)
+        -- such that f(x) =  e if phi(x)
+        -- since we do a case deduction in the definition there has to be a check that,
+        -- our domains in the case are a disjunct union of dom(f)
+        assume 
+            [Asm (TermOp DomSymbol [TermVar funVar] `Equals` TermVar domVar)
+            ,Asm (rightUniqueAdj (TermVar funVar))
+            ,Asm (relationNoun (TermVar funVar))]
+
+        goals <- gets checkingGoals
+        setGoals [makeForall [argVar] ((TermVar argVar `IsElementOf` TermVar domVar) `Iff` localFunctionGoal definitions)]
+        tellTasks
+
+        fixed <- gets fixedVars
+        assume [Asm (makeForall [argVar] ((TermVar argVar `IsElementOf` TermVar domVar) `Implies` (TermOp ApplySymbol [TermVar funVar, TermVar argVar] `IsElementOf` ranExpr)))] -- function f from \dom(f) \to \ran(f)
+        assume (functionSubdomianExpression funVar argVar domVar fixed (NonEmpty.toList definitions)) --behavior on the subdomians
+        setGoals goals
+        checkProof continue
+
+-- |Creats the Goal \forall x. x \in dom{f} \iff (phi_{1}(x) \xor (\phi_{2}(x) \xor (... \xor (\phi_{n}) ..)))
+--  where the phi_{i} are the subdomain statments
+localFunctionGoal :: NonEmpty (Term,Formula) -> Formula
+localFunctionGoal xs = makeXor $ map snd $ NonEmpty.toList xs
+
+
+-- We have our list of expr and forumlas, in this case normaly someone would write
+-- f(x) =  ....cases
+--      & (\frac{1}{k} \cdot x) &\text{if} x \in \[k, k+1\)
+--
+-- since we have to bind all globaly free Varibels we generate following asumptions.
+--
+-- For    x \mapsto  expr(x,ys,cs) , if formula(x,ys)        ; here cs are just global constants
+--          ->   \forall x,ys: ( formula(x,ys) => expr(x,ys,cs))
+ 
+
+functionSubdomianExpression :: VarSymbol -> VarSymbol -> VarSymbol -> Set VarSymbol -> [(Term, Formula)] -> [Asm]
+functionSubdomianExpression f a d s (x:xs) = singleFunctionSubdomianExpression f a d s x : functionSubdomianExpression f a d s xs
+functionSubdomianExpression _ _ _ _ [] = []
+
+singleFunctionSubdomianExpression :: VarSymbol -> VarSymbol -> VarSymbol -> Set VarSymbol -> (Term, Formula) -> Asm
+singleFunctionSubdomianExpression funVar argVar domVar fixedV (expr, frm) = let
+    -- boundVar = Set.toList (freeVars expr) in
+    -- let def = makeForall (argVar:boundVar) (((TermVar argVar `IsElementOf` TermVar domVar) `And` frm) `Implies` TermOp ApplySymbol [TermVar funVar, TermVar argVar] `Equals` expr)
+    boundVar = fixedV in    
+    let def = forallClosure boundVar (((TermVar argVar `IsElementOf` TermVar domVar) `And` frm) `Implies` (TermOp ApplySymbol [TermVar funVar, TermVar argVar] `Equals` expr))
+    in Asm def
+    
+
 
 checkCalc :: Calc -> Checking
 checkCalc calc = locally do
diff --git a/source/CommandLine.hs b/source/CommandLine.hs
index a9fb00d..b8c170e 100644
--- a/source/CommandLine.hs
+++ b/source/CommandLine.hs
@@ -18,7 +18,7 @@ import UnliftIO
 import UnliftIO.Directory
 import UnliftIO.Environment (lookupEnv)
 import System.FilePath.Posix
-
+import qualified Tptp.UnsortedFirstOrder as Syntax.Internal
 
 runCommandLine :: IO ()
 runCommandLine = do
@@ -43,10 +43,12 @@ run = do
     case withDump opts of
         WithoutDump -> skip
         WithDump dir -> do
+            liftIO (Text.putStrLn "\ESC[1;36mCreating Dumpfiles.\ESC[0m")
             let serials = [dir </> show n <.> "p" | n :: Int <- [1..]]
             tasks <- zip serials <$> encodeTasks (inputPath opts)
             createDirectoryIfMissing True dir
             forM_ tasks (uncurry dumpTask)
+            liftIO (Text.putStrLn "\ESC[35mDump ready.\ESC[0m")
     case (withParseOnly opts, withMegalodon opts) of
         (WithParseOnly, _) -> do
             ast <- parse (inputPath opts)
@@ -60,6 +62,7 @@ run = do
             -- A custom E executable can be configured using environment variables.
             -- If the environment variable is undefined we fall back to the
             -- a globally installed E executable.
+            liftIO (Text.putStrLn "\ESC[1;96mStart of verification.\ESC[0m")
             vampirePathPath <- (?? "vampire") <$> lookupEnv "NAPROCHE_VAMPIRE"
             eproverPath <- (?? "eprover") <$> lookupEnv "NAPROCHE_EPROVER"
             let prover = case withProver opts of
@@ -69,23 +72,43 @@ run = do
                     WithDefaultProver -> Provers.vampire vampirePathPath
             let proverInstance = prover Provers.Silent (withTimeLimit opts) (withMemoryLimit opts)
             result <- verify proverInstance (inputPath opts)
-            liftIO case result of
-                VerificationSuccess -> (Text.putStrLn "Verification successful.")
-                VerificationFailure [] -> error "Empty verification fail"
-                VerificationFailure ((_, proverAnswer) : _) -> case proverAnswer of
-                    Yes ->
-                        skip
-                    No tptp -> do
-                        putStrLn "Verification failed: prover found countermodel"
-                        Text.hPutStrLn stderr tptp
-                    ContradictoryAxioms tptp -> do
-                        putStrLn "Verification failed: contradictory axioms"
-                        Text.hPutStrLn stderr tptp
-                    Uncertain tptp -> do
-                        putStrLn "Verification failed: out of resources"
-                        Text.hPutStrLn stderr tptp
-                    Error err ->
-                        Text.hPutStrLn stderr err
+            case withFailList opts of
+                WithoutFailList -> liftIO case result of
+                    VerificationSuccess -> putStrLn "Verification successful."
+                    VerificationFailure [] -> error "Empty verification fail"
+                    VerificationFailure ((_, proverAnswer) : _) -> case proverAnswer of
+                        Yes ->
+                            skip
+                        No tptp -> do
+                            putStrLn "Verification failed: prover found countermodel"
+                            Text.hPutStrLn stderr tptp
+                        ContradictoryAxioms tptp -> do
+                            putStrLn "Verification failed: contradictory axioms"
+                            Text.hPutStrLn stderr tptp
+                        Uncertain tptp -> do
+                            putStrLn "Verification failed: out of resources"
+                            Text.hPutStrLn stderr tptp
+                        Error err tptp task -> do
+                            putStr "Error at:"
+
+                            Text.putStrLn task
+                            Text.putStrLn err
+                            Text.putStrLn tptp
+                            
+                WithFailList -> liftIO case result of
+                    VerificationSuccess -> putStrLn "\ESC[32mVerification successful.\ESC[0m"
+                    VerificationFailure [] -> error "Empty verification fail"
+                    VerificationFailure fails -> do
+                        putStrLn "\ESC[35mFollowing task couldn't be solved by the ATP: \ESC[0m"
+                        traverse_ showFailedTask fails
+                        Text.hPutStrLn stderr "Don't give up!"
+
+
+
+
+
+
+
 
 
 
@@ -104,6 +127,7 @@ parseOptions = do
     withVersion <- withVersionParser
     withMegalodon <- withMegalodonParser
     withDumpPremselTraining <- withDumpPremselTrainingParser
+    withFailList <- withFailListParser
     pure Options{..}
 
 withTimeLimitParser :: Parser Provers.TimeLimit
@@ -160,3 +184,7 @@ withDumpPremselTrainingParser = flag' WithDumpPremselTraining (long "premseldump
 withMegalodonParser :: Parser WithMegalodon
 withMegalodonParser = flag' WithMegalodon (long "megalodon" <> help "Export to Megalodon.")
     <|> pure WithoutMegalodon -- Default to using the cache.
+
+withFailListParser :: Parser WithFailList
+withFailListParser = flag' WithFailList (long "list_fails" <> help "Will list all unproven task with possible reason of failure.")
+    <|> pure WithoutFailList -- Default to using the cache.
\ No newline at end of file
diff --git a/source/Meaning.hs b/source/Meaning.hs
index 834d8a6..00a944f 100644
--- a/source/Meaning.hs
+++ b/source/Meaning.hs
@@ -605,9 +605,22 @@ glossProof = \case
         if domVar == argVar
             then Sem.DefineFunction funVar argVar <$> glossExpr valueExpr <*> glossExpr domExpr <*> glossProof proof
             else error "mismatched variables in function definition."
+    
+    Raw.DefineFunctionLocal funVar domVar ranExpr funVar2 argVar definitions proof -> do
+        if funVar == funVar2
+            then Sem.DefineFunctionLocal funVar argVar domVar <$> glossExpr ranExpr <*> (glossLocalFunctionExprDef `each` definitions) <*> glossProof proof
+            else error "missmatched function names"
     Raw.Calc calc proof ->
         Sem.Calc <$> glossCalc calc <*> glossProof proof
 
+
+glossLocalFunctionExprDef :: (Raw.Expr, Raw.Formula) -> Gloss (Sem.Term, Sem.Formula)
+glossLocalFunctionExprDef (definingExpression, localDomain) = do
+    e <- glossExpr definingExpression
+    d <- glossFormula localDomain
+    pure (e,d)
+
+
 glossCase :: Raw.Case -> Gloss Sem.Case
 glossCase (Raw.Case caseOf proof) = Sem.Case <$> glossStmt caseOf <*> glossProof proof
 
diff --git a/source/Provers.hs b/source/Provers.hs
index 203ee82..37e02ca 100644
--- a/source/Provers.hs
+++ b/source/Provers.hs
@@ -110,7 +110,7 @@ data ProverAnswer
     | No Text
     | ContradictoryAxioms Text
     | Uncertain Text
-    | Error Text
+    | Error Text Text Text
     deriving (Show, Eq)
 
 nominalDiffTimeToText :: NominalDiffTime -> Text
@@ -163,4 +163,4 @@ recognizeAnswer Prover{..} task tptp answer answerErr =
         | saidNo -> No tptp
         | doesNotKnow -> Uncertain tptp
         | warned -> ContradictoryAxioms tptp
-        | otherwise -> Error (answer <> answerErr)
+        | otherwise -> Error (answer <> answerErr) tptp (Text.pack(show (taskConjectureLabel task)))
diff --git a/source/Syntax/Abstract.hs b/source/Syntax/Abstract.hs
index 4aa8623..c8022c7 100644
--- a/source/Syntax/Abstract.hs
+++ b/source/Syntax/Abstract.hs
@@ -369,6 +369,13 @@ data Proof
     -- ^ Local function definition, e.g. /@Let $f(x) = e$ for $x\\in d$@/.
     -- The first 'VarSymbol' is the newly defined symbol, the second one is the argument.
     -- The first 'Expr' is the value, the final variable and expr specify a bound (the domain of the function).
+    
+    
+    
+    
+    | DefineFunctionLocal VarSymbol VarSymbol Expr VarSymbol VarSymbol (NonEmpty (Expr, Formula)) Proof
+    -- ^ Local function definition, but in this case we give the domain and target an the rules for $xs$ in some sub domains.
+    -- 
     deriving (Show, Eq, Ord)
 
 -- | An inline justification.
diff --git a/source/Syntax/Adapt.hs b/source/Syntax/Adapt.hs
index 3a8b3d6..4b43bc6 100644
--- a/source/Syntax/Adapt.hs
+++ b/source/Syntax/Adapt.hs
@@ -27,13 +27,15 @@ scanChunk ltoks =
         matchOrErr re env pos = match re toks ?? error ("could not find lexical pattern in " <> env <> " at " <> sourcePosPretty pos)
     in case ltoks of
         Located{startPos = pos, unLocated = BeginEnv "definition"} : _ ->
-            matchOrErr definition "definition" (pos)
+            matchOrErr definition "definition" pos
         Located{startPos = pos, unLocated = BeginEnv "abbreviation"} : _ ->
             matchOrErr abbreviation "abbreviation" pos
         Located{startPos = pos, unLocated = (BeginEnv "struct")} :_ ->
             matchOrErr struct "struct definition" pos
         Located{startPos = pos, unLocated = (BeginEnv "inductive")} :_ ->
             matchOrErr inductive "inductive definition" pos
+        --Located{startPos = pos, unLocated = (BeginEnv "signature")} :_ ->
+        --    matchOrErr signatureIntro "signature" pos
         _ -> []
 
 adaptChunks :: [[Located Token]] -> Lexicon -> Lexicon
@@ -85,6 +87,18 @@ abbreviation = do
     skipUntilNextLexicalEnv
     pure [lexicalItem m]
 
+signatureIntro ::  RE Token [ScannedLexicalItem]  --since signiture is a used word of haskell we have to name it diffrentliy 
+signatureIntro = do
+    sym (BeginEnv "signature")
+    few notEndOfLexicalEnvToken
+    m <- label
+    few anySym
+    lexicalItem <- head
+    few anySym
+    sym (EndEnv "signature")
+    skipUntilNextLexicalEnv
+    pure [lexicalItem m]
+
 label :: RE Token Marker
 label = msym \case
     Label m -> Just (Marker m)
diff --git a/source/Syntax/Concrete.hs b/source/Syntax/Concrete.hs
index b51b738..9b947b0 100644
--- a/source/Syntax/Concrete.hs
+++ b/source/Syntax/Concrete.hs
@@ -351,8 +351,42 @@ grammar lexicon@Lexicon{..} = mdo
 
     define           <- rule $ Define <$> (_let *> beginMath *> varSymbol <* _eq) <*> expr <* endMath <* _dot <*> proof
     defineFunction   <- rule $ DefineFunction <$> (_let *> beginMath *> varSymbol) <*> paren varSymbol <* _eq <*>  expr <* endMath <* _for <* beginMath <*> varSymbol <* _in <*> expr <* endMath <* _dot <*> proof
+    
 
-    proof            <- rule $ asum [byContradiction, byCases, bySetInduction, byOrdInduction, calc, subclaim, assume, fix, take, have, suffices, define, defineFunction, qed]
+
+
+
+
+    -- Define $f $\fromTo{X}{Y} such that,         
+    -- Define function $f: X \to Y$,
+    -- \begin{align}
+    --      &x \mapsto 3*x      &,  
+    --      &x \mapsto 4*k    &,    \forall k \in \N. x \in \Set{k}
+    -- \end{align}
+    -- 
+
+    -- Follwing is the definition right now.
+    -- Define function $f: X \to Y$ such that,
+    -- \begin{cases}
+    --     1 & \text{if } x \in \mathbb{Q}\\
+    --     0 & \text{if } x \in \mathbb{R}\setminus\mathbb{Q}
+    --     3 & \text{else}     
+    -- \end{cases}
+
+    functionDefineCase <- rule $ (,) <$> (optional _ampersand *> expr) <*> (_ampersand *> text _if *> formula)
+    defineFunctionLocal <-  rule    $ DefineFunctionLocal 
+                                    <$> (_define *> beginMath *> varSymbol)           -- Define $ f
+                                    <*> (_colon *> varSymbol)                           -- : 'var' \to 'var'
+                                    <*> (_to *> expr <* endMath <* _suchThat) 
+                                    -- <*> (_suchThat  *> align (many1 ((_ampersand *> varSymbol <* _mapsto) <*> exprApp <*> (_ampersand *> formula))))
+                                    -- <*> (_suchThat  *> align (many1 (varSymbol <* exprApp <*  formula)))
+                                    <*> (beginMath *> varSymbol) <*> (paren varSymbol <* _eq )
+                                    <*> cases (many1 functionDefineCase) <* endMath <* optional _dot 
+                                    <*> proof
+
+
+
+    proof            <- rule $ asum [byContradiction, byCases, bySetInduction, byOrdInduction, calc, subclaim, assume, fix, take, have, suffices, define, defineFunction, defineFunctionLocal, qed]
 
 
     blockAxiom  <- rule $ uncurry3 BlockAxiom     <$> envPos  "axiom" axiom
@@ -436,7 +470,6 @@ enumeratedMarked1 p = begin "enumerate" *> many1 ((,) <$> (command "item" *> lab
 
 
 
-
 -- This function could be rewritten, so that it can be used directly in the grammar,
 -- instead of with specialized variants.
 --
@@ -611,6 +644,9 @@ group body = token InvisibleBraceL *> body <* token InvisibleBraceR <?> "\"{...}
 align :: Prod r Text (Located Token) a -> Prod r Text (Located Token) a
 align body = begin "align*" *> body <* end "align*"
 
+cases :: Prod r Text (Located Token) a -> Prod r Text (Located Token) a
+cases body = begin "cases" *> body <* end "cases"
+
 
 maybeVarToken :: Located Token -> Maybe VarSymbol
 maybeVarToken ltok = case unLocated ltok of
diff --git a/source/Syntax/Concrete/Keywords.hs b/source/Syntax/Concrete/Keywords.hs
index 135cdac..b507e7e 100644
--- a/source/Syntax/Concrete/Keywords.hs
+++ b/source/Syntax/Concrete/Keywords.hs
@@ -108,7 +108,7 @@ _either = word "either" ? "either"
 _equipped :: Prod r Text (Located Token) SourcePos
 _equipped = (word "equipped" <|> word "together") <* word "with" ? "equipped with"
 _every :: Prod r Text (Located Token) SourcePos
-_every = (word "every") ? "every"
+_every = word "every" ? "every"
 _exist :: Prod r Text (Located Token) SourcePos
 _exist = word "there" <* word "exist" ? "there exist"
 _exists :: Prod r Text (Located Token) SourcePos
@@ -124,7 +124,7 @@ _for = word "for" ? "for"
 _forAll :: Prod r Text (Located Token) SourcePos
 _forAll = (word "for" <* word "all") <|> word "all" ? "all"
 _forEvery :: Prod r Text (Located Token) SourcePos
-_forEvery = (word "for" <* word "every") <|> (word "every") ? "for every"
+_forEvery = (word "for" <* word "every") <|> word "every" ? "for every"
 _have :: Prod r Text (Located Token) SourcePos
 _have = word "we" <* word "have" <* optional (word "that") ? "we have"
 _if :: Prod r Text (Located Token) SourcePos
@@ -220,3 +220,9 @@ _in :: Prod r Text (Located Token) SourcePos
 _in = symbol "∈" <|> command "in" ? "\\in"
 _subseteq :: Prod r Text (Located Token) SourcePos
 _subseteq = command "subseteq" ? "\\subseteq"
+_to :: Prod r Text (Located Token) SourcePos
+_to = command "to" ? "\\to"
+_mapsto :: Prod r Text (Located Token) SourcePos
+_mapsto = command "mapsto" ? "\\mapsto"
+_ampersand :: Prod r Text (Located Token) SourcePos
+_ampersand = symbol "&" ? "&"
\ No newline at end of file
diff --git a/source/Syntax/Internal.hs b/source/Syntax/Internal.hs
index 44603ad..c098380 100644
--- a/source/Syntax/Internal.hs
+++ b/source/Syntax/Internal.hs
@@ -324,6 +324,16 @@ makeDisjunction = \case
     [] -> Bottom
     es -> List.foldl1' Or es
 
+makeIff :: [ExprOf a] -> ExprOf a
+makeIff = \case
+    [] -> Bottom
+    es -> List.foldl1' Iff es
+    
+makeXor :: [ExprOf a] -> ExprOf a
+makeXor = \case
+    [] -> Bottom
+    es -> List.foldl1' Xor es
+
 finiteSet :: NonEmpty (ExprOf a) -> ExprOf a
 finiteSet = foldr cons EmptySet
     where
@@ -436,6 +446,8 @@ data Proof
     | Define VarSymbol Term Proof
     | DefineFunction VarSymbol VarSymbol Term Term Proof
 
+    | DefineFunctionLocal VarSymbol VarSymbol VarSymbol Term (NonEmpty (Term, Formula)) Proof
+
 deriving instance Show Proof
 deriving instance Eq   Proof
 deriving instance Ord  Proof
diff --git a/source/Syntax/Lexicon.hs b/source/Syntax/Lexicon.hs
index b5e4f58..4fe8730 100644
--- a/source/Syntax/Lexicon.hs
+++ b/source/Syntax/Lexicon.hs
@@ -95,6 +95,7 @@ builtinMixfix = Seq.fromList $ (HM.fromList <$>)
         builtinIdentifiers = identifier <$>
             [ "emptyset"
             , "naturals"
+            , "integers"
             , "rationals"
             , "reals"
             , "unit"
@@ -109,6 +110,9 @@ prefixOps =
     , ([Just (Command "fst"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "fst"))
     , ([Just (Command "snd"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "snd"))
     , ([Just (Command "pow"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "pow"))
+    , ([Just (Command "neg"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "neg"))
+    , ([Just (Command "inv"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "inv"))
+    , ([Just (Command "abs"), Just InvisibleBraceL, Nothing, Just InvisibleBraceR], (NonAssoc, "abs"))    
     , (ConsSymbol, (NonAssoc, "cons"))
     , (PairSymbol, (NonAssoc, "pair"))
     -- NOTE Is now defined and hence no longer necessary , (ApplySymbol, (NonAssoc, "apply"))
diff --git a/source/Syntax/Token.hs b/source/Syntax/Token.hs
index cb3f4cb..53e1e6a 100644
--- a/source/Syntax/Token.hs
+++ b/source/Syntax/Token.hs
@@ -189,6 +189,7 @@ toks = whitespace *> goNormal id <* eof
                 Nothing -> pure (f [])
                 Just t@Located{unLocated = BeginEnv "math"} -> goMath (f . (t:))
                 Just t@Located{unLocated = BeginEnv "align*"} -> goMath (f . (t:))
+                --Just t@Located{unLocated = BeginEnv "cases"} -> goMath (f . (t:))
                 Just t -> goNormal (f . (t:))
         goText f = do
             r <- optional textToken
@@ -204,6 +205,7 @@ toks = whitespace *> goNormal id <* eof
                 Nothing -> pure (f [])
                 Just t@Located{unLocated = EndEnv "math"} -> goNormal (f . (t:))
                 Just t@Located{unLocated = EndEnv "align*"} -> goNormal (f . (t:))
+                --Just t@Located{unLocated = EndEnv "cases"} -> goNormal (f . (t:))
                 Just t@Located{unLocated = BeginEnv "text"} -> goText (f . (t:))
                 Just t@Located{unLocated = BeginEnv "explanation"} -> goText (f . (t:))
                 Just t -> goMath (f . (t:))
@@ -219,12 +221,12 @@ toks = whitespace *> goNormal id <* eof
 -- | Parses a single normal mode token.
 tok :: Lexer (Located Token)
 tok =
-    word <|> var <|> symbol <|> mathBegin <|> alignBegin <|> begin <|> end <|> opening <|> closing <|> label <|> ref <|> command
+    word <|> var <|> symbol <|> mathBegin <|> alignBegin <|> casesBegin <|> begin <|> end <|> opening <|> closing <|> label <|> ref <|> command
 
 -- | Parses a single math mode token.
 mathToken :: Lexer (Located Token)
 mathToken =
-    var <|> symbol <|> number <|> begin <|> alignEnd <|> end <|> opening <|> closing <|> beginText <|> beginExplanation <|> mathEnd <|> command
+    var <|> symbol <|> number <|> begin <|> alignEnd <|> casesEnd <|> end <|> opening <|> closing <|> beginText <|> beginExplanation <|> mathEnd <|> command
 
 beginText :: Lexer (Located Token)
 beginText = lexeme do
@@ -277,6 +279,11 @@ alignBegin = guardM isTextMode *> lexeme do
     setMathMode
     pure (BeginEnv "align*")
 
+casesBegin :: Lexer (Located Token)
+casesBegin = guardM isTextMode *> lexeme do
+    Char.string "\\begin{cases}"
+    --setMathMode
+    pure (BeginEnv "cases")
 
 -- | Parses a single end math token.
 mathEnd :: Lexer (Located Token)
@@ -291,6 +298,12 @@ alignEnd = guardM isMathMode *> lexeme do
     setTextMode
     pure (EndEnv "align*")
 
+casesEnd :: Lexer (Located Token)
+casesEnd = guardM isMathMode *> lexeme do
+    Char.string "\\end{cases}"
+    --setTextMode
+    pure (EndEnv "cases")
+
 
 -- | Parses a word. Words are returned casefolded, since we want to ignore their case later on.
 word :: Lexer (Located Token)
diff --git a/source/Test/Golden.hs b/source/Test/Golden.hs
index 705aaa5..c01c249 100644
--- a/source/Test/Golden.hs
+++ b/source/Test/Golden.hs
@@ -39,6 +39,7 @@ testOptions = Api.Options
     , withTimeLimit = Provers.defaultTimeLimit
     , withVersion = Api.WithoutVersion
     , withMegalodon = Api.WithoutMegalodon
+    , withFailList = Api.WithoutFailList
     }
 
 goldenTests :: IO TestTree
diff --git a/source/TheoryGraph.hs b/source/TheoryGraph.hs
index c4887ea..e49bc1f 100644
--- a/source/TheoryGraph.hs
+++ b/source/TheoryGraph.hs
@@ -67,12 +67,12 @@ member :: FilePath -> TheoryGraph -> Bool
 member n (TheoryGraph g) = Map.member n g
 
 
--- | Add a node to the TheoryGraph. This is a noop if the node is already present in the graph.
+-- | Add a node to the TheoryGraph.
 addNode :: FilePath -> TheoryGraph -> TheoryGraph
 addNode a (TheoryGraph g) = TheoryGraph (Map.insertWith Set.union a Set.empty g)
 
 
--- | Add an edge to the TheoryGraph. This is a noop if the edge is already present in the graph.
+-- | Add an edge to the TheoryGraph. This is a loop if the edge is already present in the graph.
 addPrecedes :: Precedes FilePath -> TheoryGraph -> TheoryGraph
 addPrecedes e@(Precedes _ a') (TheoryGraph g) = addNode a' (TheoryGraph (insertTail e g))
     where
@@ -85,7 +85,9 @@ addPrecedes e@(Precedes _ a') (TheoryGraph g) = addNode a' (TheoryGraph (insertT
 singleton :: FilePath -> TheoryGraph
 singleton a = TheoryGraph (Map.singleton a Set.empty)
 
-
+-- | Construct a graph, from a list of nodes and edges. 
+-- It takes all nodes a and add the pair (a, emptyset) to the Theorygraph,
+-- afterwards it add all edges between the nodes.
 makeTheoryGraph :: [Precedes FilePath] -> [FilePath] -> TheoryGraph
 makeTheoryGraph es as = List.foldl' (flip addPrecedes) (TheoryGraph trivial) es
     where
@@ -94,6 +96,8 @@ makeTheoryGraph es as = List.foldl' (flip addPrecedes) (TheoryGraph trivial) es
 {-# INLINE makeTheoryGraph #-}
 
 
+-- | Construct a graph, from a list @x:xs@,
+-- where @x@ is a pair of theorys @(a,b)@ with @a@ gets imported in @b@.
 fromList :: [Precedes FilePath] -> TheoryGraph
 fromList es = TheoryGraph (Map.fromListWith Set.union es')
     where