Existence and Uniqueness of the Nonnegative Square Root of a Nonnegative Real Number

Let $\mathbb{R}$ be the set of real numbers, which by that definition is an ordered field, with order relation $\le$, in which every nonempty subset that is bounded above has a least upper bound. Write $0$ and $1$ for the additive and multiplicative identities of the underlying field, $-x$ for the additive inverse of $x$ and $x^{-1}$ for the multiplicative inverse of $x\ne0$; write $x-y=x+(-y)$ and $x^{2}=x\cdot x$.

Let $a\in\mathbb{R}$ satisfy $0\le a$. Then there is exactly one $r\in\mathbb{R}$ such that