The Cauchy-sequence reals have the least-upper-bound property

Fix $s_0 \in S$ (possible as $S \ne \emptyset$); by [L6] choose a real $a_0 < s_0$, so $a_0$ is not an upper bound of $S$, and put $b_0 = U$, an upper bound of $S$.

Define $(a_k), (b_k)$ by bisection: given $a_k$ (not an upper bound) and $b_k$ (an upper bound), let $m = (a_k + b_k)/2$; if $m$ is an upper bound set $a_{k+1} = a_k, b_{k+1} = m$, otherwise set $a_{k+1} = m, b_{k+1} = b_k$.

An induction on $k$ shows each $b_k$ is an upper bound of $S$, each $a_k$ is not, $a_k \le a_{k+1} \le b_{k+1} \le b_k$, and $b_k - a_k = (b_0 - a_0)/2^k$.

Given rational $\varepsilon > 0$, by [L4] choose $k$ with $(b_0 - a_0) < 2^k \hat\varepsilon$; then for all $j \ge k$, $b_j - a_j = (b_0 - a_0)/2^j \le (b_0 - a_0)/2^k < \hat\varepsilon$.

For $j, l \ge k$ both $a_j, a_l, b_j, b_l$ lie in the nested interval $[a_k, b_k]$, so $|a_j - a_l| \le b_k - a_k < \hat\varepsilon$ and likewise $|b_j - b_l| < \hat\varepsilon$; hence $(a_k)$ and $(b_k)$ are Cauchy sequences of reals.

By [L2], $(a_k)$ converges to a real $s$ and $(b_k)$ to a real $s'$. If $s < s'$, choose by [L6] a positive rational $\varepsilon$ with $3\hat\varepsilon < s'-s$. For all large $k$, convergence and step 4.1 give $|a_k-s| < \hat\varepsilon$, $|b_k-s'| < \hat\varepsilon$ and $b_k-a_k < \hat\varepsilon$, whence $s'-s \le |s'-b_k|+(b_k-a_k)+|a_k-s| < 3\hat\varepsilon$, a contradiction. If $s' < s$, choose $2\hat\varepsilon < s-s'$; for all large $k$, $a_k \le b_k$ and the two convergence bounds give $s-s' \le |s-a_k|+(a_k-b_k)+|b_k-s'| < 2\hat\varepsilon$, again a contradiction. Thus $s=s'$. For fixed $k$ and every $j \ge k$, step 3.1 gives $a_k \le a_j \le b_j \le b_k$. If $s<a_k$, choose $0<\hat\varepsilon<a_k-s$ and use $a_j\to s$; if $b_k<s$, choose $0<\hat\varepsilon<s-b_k$ and use $b_j\to s$. Each choice contradicts the displayed inequalities for all large $j$, so $a_k \le s \le b_k$.

Every $t \in S$ satisfies $t \le b_k$ for all $k$, since each $b_k$ is an upper bound. If $s<t$, choose by [L6] a positive rational $\varepsilon$ with $\hat\varepsilon<t-s$. Since $b_k\to s$, eventually $|b_k-s|<\hat\varepsilon$, hence $b_k<s+\hat\varepsilon<t$, contradicting $t\le b_k$. Therefore $t\le s$, so $s$ is an upper bound of $S$.

If $v$ is any upper bound of $S$, then for each $k$ some element of $S$ exceeds $a_k$, because $a_k$ is not an upper bound; hence $a_k<v$. If $v<s$, choose by [L6] a positive rational $\varepsilon$ with $\hat\varepsilon<s-v$. Since $a_k\to s$, eventually $|a_k-s|<\hat\varepsilon$, so $a_k>s-\hat\varepsilon>v$, a contradiction. Thus $s\le v$, and $s$ is the least upper bound.

Hence $s = \sup S$ exists in $\mathbb{R}_C$; as $S$ was an arbitrary nonempty bounded-above set, $\mathbb{R}_C$ has the least-upper-bound property and is a complete ordered field.