Theorem: Topological Subspace of Real Number Line is Lindelöf

Let $\struct {\R, \tau_d}$ be the real number line with the usual (Euclidean) topology.
Let $W$ be a non-empty subset of $\R$.
Then $R_W$ is Lindelöf
where $R_W$ denotes the topological subspace of $R$ on $W$.

Proof:
Let $\CC$ be a open cover for $W$.
Define $Q := \set {\openint a b: a, b \in \Q}$
Define a mapping $h: Q \to \Q \times \Q$:
:$\forall \openint a b \in Q: \map h {\openint a b} = \tuple {a, b}$
It is easy to see by definition that
:$h$ is an injection.
By Injection iff Cardinal Inequality:
:$\card Q \le \card {\Q \times \Q}$
where $\card Q$ deontes the cardinality of $Q$.
By Rational Numbers are Countably Infinite:
:$\Q$ is countably infinite.
By definition of countably infinite:
:there exists a bijection $\Q \to \N$
By definitions of set equality and cardinality:
:$\card \Q = \card \N$
By Aleph Zero equals Cardinality of Naturals:
:$\card \Q = \aleph_0$
By Cardinal Product Equal to Maximum:
:$\card {\Q \times \Q} = \max \set {\aleph_0, \aleph_0} = \aleph_0$
By Countable iff Cardinality not greater than Aleph Zero:
:$Q$ is countable.
By definition of cover:
:$W \subseteq \bigcup \CC$
By definition of imion:
:$\forall x \in W: \exists U \in \CC: x \in U$
By Axiom of Choice define a mapping $f: W \to \CC$:
:$\forall x \in W: x \in \map f x$
We will prove that
:$\forall x \in W: \exists A \in Q: x \in A \land A \cap W \subseteq \map f x$
Let $x \in W$.
By definition of open cover:
:$\map f x$ is open in $R_W$.
By definition of topological subspace:
:there exists U a subset of $\R$ such that
::$U$ is open in $R$ and $U \cap W = \map f x$
By definition of $f$:
:$x \in \map f x$
By definition of open set in metric space:
:$\exists r > 0: \map {B_r} x \subseteq U$
:$\openint {x - r} {x + r} \subseteq U$
By Between two Real Numbers exists Rational Number:
:$\exists q \in \Q: x - r < q < x$ and $\exists p \in \Q: x < p < x + r$
By definition of $Q$:
:$\openint q p \in Q$
Thus by definition of open real interval:
:$x \in \openint q p \subseteq \openint {x - r} {x + r}$
By Subset Relation is Transitive:
:$\openint q p \subseteq U$
Thus by Set Intersection Preserves Subsets/Corollary:
:$\openint q p \cap W \subseteq \map f x$
By Axiom of Choice define a mapping $f_1: W \to Q$:
:$\forall x \in W: x \in \map {f_1} x \land \map {f_1} x \cap W \subseteq \map f x$
By definitions of image of set and image of mapping:
:$\forall A \in \Img {f_1}: \exists x \in W: x \in f_1^{-1} \sqbrk {\set A}$
By Axiom of Choice define a mapping $c: \Img {f_1} \to W$:
:$\forall A \in \Img {f_1}: \map c A \in f_1^{-1} \sqbrk {\set A}$
Define a mapping $g: \Img {f_1} \to \CC$:
:$g := f \circ c$
Define $\GG = \Img g$.
Thus $\GG \subseteq \CC$
By definition of image of mapping:
:$\Img {f_1} \subseteq Q$
By Subset of Countable Set is Countable;
:$\Img {f_1}$ is countable.
By Surjection iff Cardinal Inequality:
:$\size {\Img g} \le \size {\Img {f_1} }$
Thus by Countable iff Cardinality not greater than Aleph Zero:
:$\GG$ is countable.
It remains to prove that
:$\GG$ is a cover for $W$.
Let $x \in W$.
By definition of $f_1$:
:$ x \in \map {f_1} x \land \map {f_1} x \cap W \subseteq \map f x$
By definition of image of mapping:
:$\map {f_1} x \in \Img {f_1}$
Then by definition of $c$:
:$y := \map c {\map {f_1} x} \in f_1^{-1} \sqbrk {\set {\map {f_1} x} }$
By definition of $f_1$:
:$y \in \map {f_1} y \land \map {f_1} y \cap W \subseteq \map f y$
By definition of image of set:
:$\map {f_1} y = \map {f_1} x$
Then by definitions of subset and intersection:
:$x \in \map f y$
By definition of composition of mappings:
:$\map f y = \map g {\map {f_1} x}$
By definition of image of mapping:
:$\map g {\map {f_1} x} \in \GG$
Thus by definition of union:
:$x \in \bigcup \GG$
Thus the result.
{{qed}}