consider b being Sqrt of a such that
A: not b is O -negative by lemsqrtex;
reconsider b = b as non O -negative Sqrt of a by A;
take b ; :: thesis: b ^2 = a
thus b ^2 = a by defsqrt; :: thesis: verum