let a, b be Real; :: thesis: ( a >= 0 implies sqrt (a + (b ^2)) >= b )
assume A1: a >= 0 ; :: thesis: sqrt (a + (b ^2)) >= b

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

suppose b < 0 ; :: thesis: sqrt (a + (b ^2)) >= b

hence sqrt (a + (b ^2)) >= b by A1, Def2; :: thesis: verum

end;

suppose A2: b >= 0 ; :: thesis: sqrt (a + (b ^2)) >= b

A3: b ^2 >= 0 by XREAL_1:63;
a + (b ^2) >= 0 + (b ^2) by A1, XREAL_1:6;
then sqrt (a + (b ^2)) >= sqrt (b ^2) by A3, Th26;
hence sqrt (a + (b ^2)) >= b by A2, Def2; :: thesis: verum

end;

end;