Theorem: Sorgenfrey Line is Lindelöf

The Sorgenfrey line is a Lindelöf space.

Proof:
Let $T = \struct {\R, \tau}$ be the Sorgenfrey line.
Let $\CC$ be an open cover for $\R$.
Define $\VV = \set {U^\circ_\R: U \in \CC}$
where $U^\circ_\R$ denotes the interior of $U$ in the real number line $R = \struct {\R, \tau_d}$ with the usual (Euclidean) topology.
By definition of interior:
:$\forall U \in \CC: U^\circ_\R \subseteq \R$
By Union is Smallest Superset:
:$W := \bigcup \VV \subseteq \R$ 
By Topological Subspace of Real Number Line is Lindelöf:
:$R_W$ is Lindelöf
where $R_W$ denotes topological subspace of $R$ on $W$.
By Set is Subset of Union/Set of Sets:
:$\forall A \in \VV: A \subseteq W$
By Intersection with Subset is Subset:
:$\forall A \in \VV: A \cap W = A$
By definition of topological subspace:
:$\forall A \in \VV: A$ is open in $R_W$
By definition
:$\VV$ is open cover
By definition of Lindelöf space:
:there exists a countable subcover $\SS$ of $\VV$
By definition of $\VV$:
:$\forall A \in \VV: \exists U \in \CC: A = U^\circ_\R$
By {{Axiom-link|Choice}} define a mapping $g: \VV \to \C C$:
:$\forall A \in \VV: A = \map g A^\circ_\R$
Define $K = \map {g^\to} \SS$
where $\map {g^\to} \SS$ denotes the image of $\SS$ under $g$.
Define $Y := \R \setminus \bigcup K$
By definition of cover:
:$\R \subseteq \bigcup \CC$
By definition of subset:
:$\forall x \in \R: x \in \bigcup \CC$
By definition of union:
:$\forall x \in \R: \exists U \in \CC: x \in U$
By {{Axiom-link|Choice}} define a mapping $f: \R \to \CC$ such that
:$\forall x \in \R: x \in \map f x$
Define $\BB := \set {\hointr x y: x, y \in \R}$
By definition of the Sorgenfrey line:
:$\BB$ is a basis of $T$.
By definition of $f$:
:$\forall x \in \R: \map f x \in \CC$
By definition of open cover:
:$\forall x \in \R: \map f x$ is open
By definition of a basis:
:$\forall x \in \R: \exists U_x \in \BB: x \in U_x \subseteq \map f x$
By definition of $\BB$:
:$\forall x \in \R: \exists y, z \in \R: x \in \hointr y z \subseteq \map f x$
By definition of half-open real interval:
:$\forall x \in \R: \exists z \in \R: x \in \hointr x z \subseteq \map f x$
By {{Axiom-link|Choice}} define a mapping $k: \R \to \BB$:
:$\forall x \in \R: \exists z \in \R: x \in \map k x = \hointr x z \subseteq \map f x$
We will prove that
:$(1): \quad \forall x, y \in Y: x \ne y \implies \paren x \cap \map k y = \O$
{{Mistake|For $\paren x$ should it really be $\map k x$?}}
Let $x, y \in Y$ such that $x \ne y$.
{{AimForCont}}:
:$\paren x \cap \map k y \ne \O$
By definitions of empty set and intersection:
:$\exists s: s \in \map k x \land s \in \map k y$
By definition of $k$:
:$\exists z_1 \in \R: \map k x = \hointr x {z_1} \subseteq \map f x$
and
:$\exists z_2 \in \R: \map k y = \hointr y {z_2}$
By Trichotomy Law for Real Numbers:
:$x < y$ or $x > y$
{{WLOG}}, suppose $x < y$
By definition of half-open real interval:
:$x \le s < z_1$ and $y \le s < z_2$
Then:
$y < z_1$
By definition of open real interval:
:$y \in \openint x {z_1}$
By Open Real Interval is Open Set:
:$\openint x {z_1}$ is topologically open in $R$
By definition of subset:
:$\openint x {z_1} \subseteq \hointr x {z_1}$
By Subset Relation is Transitive:
:$\openint x {z_1} \subseteq \map f x$
By Interior of Subset:
:$\openint x {z_1}^\circ_\R \subseteq \map f x^\circ_\R$
By Interior of Open Set:
:$\openint x {z_1}^\circ_\R \openint x z_1$
{{mistake|The relation is missing in the above -- subset or equals? Research needed}}
By definition of subset:
:$y \in \map f x^\circ_\R$
By definition of $\VV$:
:$\map f x^\circ_\R \in \VV$
By definition of union:
$y \in W$
By definition of interior:
:$\forall A \in \SS: A \subseteq \map g A$
By Set Union Preserves Subsets:
:$W \subseteq \bigcup \SS \subseteq \bigcup K$
By definition of subset:
:$y \in \bigcup K$
This contradicts $y \in Y$ by definition of difference.
Thus:
:$\map k x \cap \map k y = \O$
By Set of Pairwise Disjoint Intervals is Countable
:$\map {k^\to} Y$ is countable
We will prove that
:$k \restriction_Y$ is an injection
Let $x, y \in Y$ such that
:$\map {k \restriction_Y} x = \map {k \restriction_Y} Y$
{{AimForCont}}:
:$x \ne y$
Then by $(1)$:
:$\map k x \cap \map k y = \O$
By definition of restriction of mapping:
:$\map {k \restriction_Y} x = \map k x$
and
:$\map {k \restriction_Y} y = \map k y$
By definition of $k$:
:$x \in \map k x$
So:
:$x \in \map k y$
This contradicts:
:$\map k x \cap \map k y = \O$
Thus $x = y$.
By Injection to Image is Bijection:
:$k \restriction_Y: Y \to \map {k^\to} Y$ is a bijection
By definitions of set equivalence and cardinality:
:$\card Y = \card {\map {k^\to} Y}$
where $\card Y$ denotes the cardinality of $Y$.
By Cardinality of Image of Set not greater than Cardinality of Set:
:$\card K \le \card \SS$ and $\card {\map {f^\to} Y} \le \card Y$
By Countable iff Cardinality not greater than Aleph Zero:
:$\card \SS \le \aleph_0$ and $\card Y \le \aleph_0$
Then:
:$\card K \le \aleph_0$ and $\card {\map {f^\to} Y} \le \aleph_0$
By Countable iff Cardinality not greater than Aleph Zero:
:$K$ is countable and $\map {f^\to} Y$ is countable
Thus by Countable Union of Countable Sets is Countable:
:$\GG := K \cup \map {f^\to} Y$ is countable
By definition of image of set:
:$K \subseteq \CC$ and $\map {f^\to} Y \subseteq \CC$
thus by {{Corollary|Set Union Preserves Subsets}}:
:$\GG \subseteq \CC$
It remains to prove that
:$\GG$ is cover for $\R$
Let $x \in \R$.
By Set Union is Self-Distributive: Sets of Sets:
:$\bigcup \GG = \paren {\bigcup K} \cup \bigcup \map {f^\to} Y$
{{AimForCont}}:
:$x \notin \bigcup \GG$
By definition of union:
:$x \notin \bigcup K$ and $x \notin \bigcup \map {f^\to} Y$
By definition of difference:
:$x \in Y$
By definition of image of set:
:$\map f x \in \map {f^\to} Y$
By definition of $f$:
:$x \in \map f x$
By definition of union:
:$x \in \bigcup \map {f^\to} Y$
This contradicts $x \notin \bigcup \map {f^\to} Y$.
Thus the result by Proof by Contradiction.
{{qed}}
{{AoC}}