The Dedekind reals form a totally ordered field

By Inclusion totally orders the Dedekind reals the relation $\subseteq$ is a reflexive, antisymmetric, transitive, and total order on $\mathbb{R}$.

Translation invariance: suppose $A\subseteq B$. Every element of $A+C$ has the form $a+c$ with $a\in A$, $c\in C$; since $a\in A\subseteq B$, also $a+c\in B+C$. Hence $A+C\subseteq B+C$, i.e. $A\le B\Rightarrow A+C\le B+C$.

Positivity of products of nonnegatives: suppose $0^{\ast }\le A$ and $0^{\ast }\le B$. If $A=0^{\ast }$ or $B=0^{\ast }$, then $A\cdot B=0^{\ast }$ by the sign rule [L4], so $0^{\ast }\subseteq A\cdot B$. Otherwise $A,B>0^{\ast }$, and the positive-case formula [L4] gives $A\cdot B\supseteq \{q\in \mathbb{Q}:q\le 0\}\supseteq \{r\in \mathbb{Q}:r<0\}=0^{\ast }$, so $0^{\ast }\subseteq A\cdot B$. In either case $0^{\ast }\le A\cdot B$.

Thus $\mathbb{R}$ is a field whose inclusion order is total, translation-invariant, and closed under multiplication of nonnegative cuts: a totally ordered field.