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

Let $\mathbb{R}$ be the set of \reftext{def:real-numbers-c54-2026c}{real numbers}, which by that definition is an \reftext{def:ordered-field-c54-2026b}{ordered field}, with order relation $\le$, in which every nonempty subset that is bounded above has a \reftext{def:upper-bound-supremum-c54-2026b}{least upper bound}. Write $0$ and $1$ for the additive and multiplicative identities of the underlying \reftext{def:field-c54-2026b}{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