let a, b be Real; :: thesis: ( a >= b ^2 implies sqrt a >= b )
assume A1: a >= b ^2 ; :: thesis: sqrt a >= b
b ^2 >= 0 by XREAL_1:63;
then A2: sqrt a >= sqrt (b ^2) by A1, SQUARE_1:26;

per cases ( b >= 0 or b < 0 ) ;

suppose b >= 0 ; :: thesis: sqrt a >= b

hence sqrt a >= b by A2, SQUARE_1:22; :: thesis: verum

end;

suppose A3: b < 0 ; :: thesis: sqrt a >= b

then sqrt a >= - b by A2, SQUARE_1:23;
hence sqrt a >= b by A3; :: thesis: verum

end;

end;