The Sorgenfrey line: $\mathbb{R}$ with the half-open intervals $[a,b)$ as a basis is strictly finer than the usual topology, is first countable, has a countable dense subset, and its sequences converge only from the right

$\mathcal{B}$ covers $\mathbb{R}$: for $x \in \mathbb{R}$ one has $x < x + 1$ by [L4], so $[x,\ x+1) \in \mathcal{B}$ and $x \in [x, x+1)$.

Let $x \in [a,b) \cap [c,d)$ and put $a' := \max\{a,c\}$ and $b' := \min\{b,d\}$, which exist by [L4]. Then $[a,b) \cap [c,d) = [a',b')$, since $a \le t$ and $c \le t$ together say $a' \le t$ and $t < b$ with $t < d$ says $t < b'$; and $a' \le x < b'$ gives $a' < b'$, so $[a',b') \in \mathcal{B}$ and $x \in [a',b') \subseteq [a,b) \cap [c,d)$.

For $x \in \mathbb{R}$ and real $r > 0$: $x < x + r$ by [L4], and $[x,\ x+r) \subseteq (x-r,\ x+r)$, since $x - r < x \le t < x + r$.

For every $k \in \mathbb{N}$ the real $1/(k+1)$ is positive by [L3], so $[x,\ x + 1/(k+1)) \in \mathcal{B}$ by [L4] and contains $x$.

$[0,1) \in \mathcal{B}$, since $0 < 1$ by [L4].

Every nonempty member $[a,b)$ of $\mathcal{B}$ meets $\mathbb{Q}$: by [L5] there is a rational $q$ with $a < q < b$, and then $q \in [a,b)$.

The same sequence converges to $x$ in the usual topology: given $r > 0$, [L3] gives $n \ge 1$ with $1/n < r$ and $n = m+1$; for $k \ge m$ the canonical naturals satisfy $0 < (m+1) \cdot 1_{\mathbb{R}} \le (k+1) \cdot 1_{\mathbb{R}}$, so $1/(k+1) \le 1/(m+1) < r$ by [L3], and $|y_k - x| = 1/(k+1) < r$, that is $y_k \in B(x,r)$.

By steps 1.1 and 1.2 the family $\mathcal{B}$ satisfies the two basis conditions of [L1], so it is a basis for the topology $\mathcal{T}_{\mathrm{S}}$ described there; this is claim 1.

$[0,1)$ is not open in the usual topology: for any $r > 0$, [L3] gives a natural $n \ge 1$ with $1/n < r$, and $-1/n$ satisfies $-r < -1/n < 0$, so $-1/n \in (-r, r)$ while $-1/n \notin [0,1)$; hence no ball around $0$ lies inside $[0,1)$.

The family $\{\, [x,\ x+1/(k+1)) : k \in \mathbb{N} \,\}$ is nonempty and is the image of the surjection $k \mapsto [x,\ x+1/(k+1))$ from $\mathbb{N}$, hence at most countable.

By step 1.6 the set $\mathbb{Q}$ meets every nonempty basic open set, so it is dense by [L6]; with [L5] it is at most countable, which is claim 4.

Every set $U$ open in the usual topology lies in $\mathcal{T}_{\mathrm{S}}$: for $x \in U$ take $r > 0$ with $(x-r,x+r) \subseteq U$, and then $x \in [x,\ x+r) \subseteq U$ by step 1.3, with $[x,x+r) \in \mathcal{B}$.

Let $N$ be a neighbourhood of $x$ in $\mathcal{T}_{\mathrm{S}}$ and take $[a,b) \in \mathcal{B}$ with $x \in [a,b) \subseteq N$, so $a \le x < b$ and $b - x > 0$; by [L3] fix a natural $n \ge 1$ with $1/n < b - x$ and write $n = m+1$ with $m \in \mathbb{N}$. Then $x + 1/(m+1) < b$, so $[x,\ x+1/(m+1)) \subseteq [x, b) \subseteq [a,b) \subseteq N$.

For every real $\varepsilon > 0$ the set $[x,\ x+\varepsilon)$ is a member of $\mathcal{B}$ containing $x$, hence a neighbourhood of $x$ in $\mathcal{T}_{\mathrm{S}}$.

By steps 3.1 and 2.2 the topology $\mathcal{T}_{\mathrm{S}}$ contains the usual topology and contains $[0,1)$, which the usual topology does not; so $\mathcal{T}_{\mathrm{S}}$ is strictly finer, which is claim 2.

By steps 1.4, 3.2 and 2.3 the family of claim 3 consists of neighbourhoods of $x$, is at most countable, and has a member inside every neighbourhood of $x$; so it is an at most countable neighbourhood base at $x$, and $x$ was arbitrary. This is claim 3.

If $x_k \to x$ in $\mathcal{T}_{\mathrm{S}}$ and $\varepsilon > 0$, then by step 3.3 the set $[x, x+\varepsilon)$ is a neighbourhood of $x$, so there is $K$ with $x_k \in [x, x+\varepsilon)$, that is $x \le x_k < x + \varepsilon$, for all $k \ge K$.

Conversely, assume the $\varepsilon$ condition and let $N$ be a neighbourhood of $x$; take $[a,b) \in \mathcal{B}$ with $x \in [a,b) \subseteq N$ and apply the condition with $\varepsilon := b - x > 0$, obtaining $K$ with $x \le x_k < b$ for all $k \ge K$; since $a \le x \le x_k$, this gives $x_k \in [a,b) \subseteq N$ for all $k \ge K$. So $x_k \to x$.

The sequence $y_k = x - 1/(k+1)$ satisfies $y_k < x$ for every $k$, since $1/(k+1) > 0$; so no term lies in $[x, x+1)$, and by step 4.3 with $\varepsilon = 1$ the sequence does not converge to $x$ in $\mathcal{T}_{\mathrm{S}}$.

Steps 4.3 and 4.4 give the equivalence of claim 5, and steps 5.1 and 1.7 give the sequence it names; with steps 4.1, 4.2, 2.4 and 2.1 all five claims are proved.