Construction of the Dedekind Cuts: They Form a Set Totally Ordered by Inclusion, Closed under Sums, Negatives and Products of Nonnegative Cuts

In the setting of The Integers and the Rational Numbers, with the Natural Numbers and the Integers Identified with Subsets of the Rationals, let $<$ be the strict relation of the order $\le$ of $\mathbb{Q}$, and let $C$ be the class of those subsets $x$ of $\mathbb{Q}$, that is, elements of the power set $\mathcal{P}(\mathbb{Q})$, such that $x\neq\emptyset$, $x\neq\mathbb{Q}$, every $v\in\mathbb{Q}$ with $v<u$ for some $u\in x$ lies in $x$, and every $u\in x$ has some $v\in x$ with $u<v$. Let $\le_{C}$ be the class of pairs $(x,y)$ in the Cartesian product $C\times C$ with $x\subseteq y$. For $u\in\mathbb{Q}$ and $x,y\in C$ let

$$u^{*}=\{v\in\mathbb{Q}:v<u\},\qquad x\oplus y=\{w\in\mathbb{Q}:\exists u\,\exists v\,(u\in\mathbb{Q}\wedge v\in\mathbb{Q}\wedge u\in x\wedge v\in y\wedge w=u+v)\},$$ $$\ominus x=\{u\in\mathbb{Q}:\exists v\,(v\in\mathbb{Q}\wedge0<v\wedge-u-v\notin x)\},$$ $$x\odot y=0^{*}\cup\{w\in\mathbb{Q}:\exists u\,\exists v\,(u\in\mathbb{Q}\wedge v\in\mathbb{Q}\wedge u\in x\wedge v\in y\wedge0\le u\wedge0\le v\wedge w=u\cdot v)\}.$$

¶ $C$ is a set.

¶ $\le_{C}$ is a total order on $C$.

¶ $u^{*}\in C$ for every $u\in\mathbb{Q}$.

¶ $x\oplus y\in C$ for all $x,y\in C$.

¶ $\ominus x\in C$ for every $x\in C$.

¶ For every $x\in C$, $0^{*}\subseteq x$ or $0^{*}\subseteq\ominus x$.

¶ If $x,y\in C$, $0^{*}\subseteq x$ and $0^{*}\subseteq y$, then $x\odot y\in C$ and $0^{*}\subseteq x\odot y$.