Prove that $(\sup\{y\in\Bbb R^{\ge0}:y^2\le x\})^2=x$ This question is a simple one from foundations of analysis, regarding the definition of the square root function. We begin by defining
$$\sqrt x:=\sup\{y\in\Bbb R^{\ge0}:y^2\le x\}:=\sup S(x)$$
for $x\ge0$, and now we wish to show that it satisfies its defining property, namely $\sqrt x^2=x$. By dividing into cases $x\le1$ (where $1$ is an upper bound for $S(x)$) and $x\ge1$ (where $x$ is an upper bound for $S(x)$), we know $S(x)$ is upper bounded and hence the function is well-defined for all $x\ge0$.
It follows from the intermediate value theorem applied to $f(y)=y^2$ on $[0,\max(1,x)]$ that $\sqrt x^2=x$, if we can prove that $f(y)$ is continuous, but suffice it to say that I would like to prove the IVT later in generality, when I will have the definition $|x|=\sqrt{xx^*}$ (which is used in the definition of continuity), so I hit a circularity problem. Thus I need a "bootstrap" version of the IVT for this particular case, i.e. I can't just invoke this theorem.
What is the cleanest way to get to the goal here? Assume I don't have any theorems to work from except basic algebra.

Since you have the l.u.b. axiom, you can use that, for any two bounded sets $A,B$ of nonnegative reals, we have 
$$(\sup A) \cdot (\sup B)=\sup( \{a\cdot b:a \in A,b \in B\}).$$
Applying this to $A=B=S(x)$ we want to find the sup of the set of products $a\cdot b$ where $a^2\le x$ and $b^2 \le x.$ First note any such product is at most $x$: without loss assume $a \le b$, then we have $ab \le b^2 \le x.$ This much shows $\sqrt{x}\cdot \sqrt{x} \le x$ for your definition of $\sqrt{x}$ as a sup.
Second, since we may use any (independent) choices of $a,b \in S(x)$ we may in particular take them both equal, and obtain the products $t\cdot t=t^2$ which, given the definition of $S(x)$, have supremum $x$, which shows that $\sqrt{x}\cdot \sqrt{x} \ge x$.
