consider b being Sqrt of a such that
A: not b is O -negative by lemsqrtex;
B: now :: thesis: not b = 0. R
assume b = 0. R ; :: thesis: contradiction
then 0. R = b ^2 ;
hence contradiction by defsqrt; :: thesis: verum
end;
take - b ; :: thesis: ( - b is Sqrt of a & - b is O -negative )
C: (- b) ^2 = b ^2 by VECTSP_1:10
.= a by defsqrt ;
not b < O, 0. R by A, x2;
then 0. R < O,b by B, avb4;
then - b < O, - (0. R) by c10a;
hence ( - b is Sqrt of a & - b is O -negative ) by C, defsqrt, x2; :: thesis: verum