Rename for compat

1 files changed, 989 insertions, 0 deletions

diff --git a/library/topology/urysohntwo.tex b/library/topology/urysohntwo.tex
new file mode 100644
index 0000000..a1a3ba0
--- /dev/null
+++ b/library/topology/urysohntwo.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}
+
+
+
+
+
+