Square roots exist: a unique $\sqrt{a}\ge 0$ with $(\sqrt{a}{)}^2=a$; the positives are $\{x^2:x\mathrm{\ne }0\}$

If $a=0$, then $s=0$ satisfies $s\ge 0$ and $s^2=0=a$, so existence holds; assume henceforth $a>0$.

Uniqueness holds once a root exists: if $u,v\ge 0$ satisfy $u^2=v^2$, then strict monotonicity of squaring on nonnegatives [L3] rules out both $u<v$ and $u>v$, forcing $u=v$; so at most one $s\ge 0$ has $s^2=a$.

Define $S=\{t\in F:t\ge 0\text{ and }{t}^2\le a\}$; then $0\in S$ because $0\ge 0$ and $0^2=0\le a$, so $S\mathrm{\ne }\mathrm{\varnothing }$.

The element $1+a$ is an upper bound of $S$: since $a>0$ we have $1+a>1$, so any $t>1+a$ has $t>1$ and $t>0$, whence $t^2=t\cdot t>1\cdot t=t>1+a>a$, giving $t\mathrm{\notin }S$.

By completeness [L1], $s:=\sup S$ exists in $F$; and since $0\in S$ we have $s\ge 0$.

Assume, for contradiction, that $s^2\mathrm{\ne }a$; by trichotomy either $s^2<a$ or $s^2>a$.

(Case $s^2<a$.) Since $a-s^2>0$ and $2s+1>0$, [L6] and [L2] give $c=(a-s^2)\mathrm{/}(2s+1)>0$. Let $h=c\mathrm{/}2$ if $c\le 1$, and $h=1\mathrm{/}2$ if $c>1$. Since $0<1<2$, [L6] gives $0<1\mathrm{/}2<1$; together with the ordered-field sign and scaling rules [L2], this gives $0<h<1$ and $h<c$ in either branch; then $h^2=h\cdot h<h\cdot 1=h$ and $h(2s+1)<a-s^2$, so $(s+h{)}^2=s^2+2sh+h^2<s^2+2sh+h=s^2+h(2s+1)<a$, whence $s+h\in S$ with $s+h>s$, contradicting that $s$ is an upper bound of $S$.

(Case $s^2>a$.) Here $s>0$ since $s^2>a\ge 0$; since $s^2-a>0$ and $2s>0$, [L6] and [L2] give $c=(s^2-a)\mathrm{/}(2s)>0$. Let $h=c\mathrm{/}2$ if $c\le s$, and $h=s\mathrm{/}2$ if $c>s$. Again [L6] gives $0<1\mathrm{/}2<1$, and the ordered-field sign and scaling rules [L2] give $0<h<s$ and $h<c$, so $2sh<s^2-a$ and $(s-h{)}^2=s^2-2sh+h^2\ge s^2-2sh>a$, hence every $t\in S$ has $t^2\le a<(s-h{)}^2$ with $t\ge 0$ and $s-h>0$, so $t<s-h$ by [L3]; thus $s-h$ is an upper bound of $S$ with $s-h<s$, contradicting that $s$ is the least upper bound.

Both cases of the disjunction in step 3.1 give a contradiction, so the assumption fails and $s^2=a$: a unique (by step 1.2) $s=\sqrt{a}\ge 0$ with $s^2=a$ exists, and applying this to any $x>0$ writes $x=(\sqrt{x}{)}^2$ with $\sqrt{x}\mathrm{\ne }0$ while conversely any nonzero square is positive by [L4], so the positive elements of $F$ are exactly the nonzero squares.