The rationals embed densely in the reals

Embedding: constant sequences are Cauchy; $\widehat{q}=\widehat{r}$ iff the constant $q-r$ is null iff $q=r$; operations match termwise; and $q<r$ gives the constant lower bound $r-q>0$, so $\widehat{q}<\widehat{r}$ and order is preserved and reflected.

Fix $N$ with $\mathrm{\mid }{a}_m-a_n\mathrm{\mid }<\epsilon \mathrm{/}2$ for all $m,n\ge N$, and set $q=a_N$.

The difference $\widehat{q}-x$ has representative $(a_N-a_n)$ with $\mathrm{\mid }{a}_N-a_n\mathrm{\mid }<\epsilon \mathrm{/}2$ for $n\ge N$; hence both $\widehat{\epsilon }-(x-\widehat{q})$ and $\widehat{\epsilon }-(\widehat{q}-x)$ have representatives eventually $>\epsilon \mathrm{/}2$, so both are positive: $\mathrm{\mid }x-\widehat{q}\mathrm{\mid }<\widehat{\epsilon }$.

Inverses: let $q$ be a nonzero rational. Then $\widehat{q}\mathrm{\ne }\widehat{0}=0_{\mathbb{R}}$ by the injectivity of step 1.1, and $1\mathrm{/}q$ exists in $\mathbb{Q}$ by [L2]; since the operations match termwise (step 1.1), $\widehat{q}\cdot \widehat{1\mathrm{/}q}=\widehat{q\cdot (1\mathrm{/}q)}=\widehat{1}=1_{\mathbb{R}}$. Inverses in $\mathbb{R}$ are unique by [L5], so $(\widehat{q}{)}^{-1}=\widehat{1\mathrm{/}q}$: the embedding preserves reciprocals.

Density: let $x<y$; pick $\delta >0$ rational and $N$ with the representative of $y-x$ eventually $>\delta$; set $\epsilon =\delta \mathrm{/}4$ and pick $q$ with $\mathrm{\mid }x-\widehat{q}\mathrm{\mid }<\widehat{\epsilon }$; then $q^{\mathrm{\prime }}=q+2\epsilon$ satisfies ${\widehat{q}}^{\mathrm{\prime }}-x\ge -\widehat{\epsilon }+2\widehat{\epsilon }=\widehat{\epsilon }>0$ and $y-{\widehat{q}}^{\mathrm{\prime }}\ge \widehat{\delta }-\widehat{\epsilon }-2\widehat{\epsilon }=\widehat{\delta }\mathrm{/}4>0$, so $x<{\widehat{q}}^{\mathrm{\prime }}<y$.

The rationals embed as an ordered subfield — injectively, preserving the order in both directions, the ring operations, and reciprocals — and they approximate every real arbitrarily well and separate any two reals.