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 O -positive
not b < O, 0. R by A, x2;
then 0. R < O,b by B, avb4;
hence b is O -positive by x1; :: thesis: verum