let a, b be Real; :: thesis: ( ((- a) + (sqrt ((a ^2) + (b ^2)))) / 2 >= 0 & (a + (sqrt ((a ^2) + (b ^2)))) / 2 >= 0 )
A1: b ^2 >= 0 by XREAL_1:63;
A2: a ^2 >= 0 by XREAL_1:63;
then A3: sqrt ((a ^2) + (b ^2)) >= 0 by A1, SQUARE_1:def 2;
(a ^2) + (b ^2) >= 0 + (a ^2) by A1, XREAL_1:7;
then A4: sqrt ((a ^2) + (b ^2)) >= sqrt (a ^2) by A2, SQUARE_1:26;

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

suppose A5: a >= 0 ; :: thesis: ( ((- a) + (sqrt ((a ^2) + (b ^2)))) / 2 >= 0 & (a + (sqrt ((a ^2) + (b ^2)))) / 2 >= 0 )

then sqrt ((a ^2) + (b ^2)) >= a by A4, SQUARE_1:22;
then (sqrt ((a ^2) + (b ^2))) - a >= a - a by XREAL_1:9;
hence ( ((- a) + (sqrt ((a ^2) + (b ^2)))) / 2 >= 0 & (a + (sqrt ((a ^2) + (b ^2)))) / 2 >= 0 ) by A3, A5; :: thesis: verum

end;

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

then sqrt ((a ^2) + (b ^2)) >= - a by A4, SQUARE_1:23;
then (sqrt ((a ^2) + (b ^2))) - (- a) >= (- a) - (- a) by XREAL_1:9;
hence ( ((- a) + (sqrt ((a ^2) + (b ^2)))) / 2 >= 0 & (a + (sqrt ((a ^2) + (b ^2)))) / 2 >= 0 ) by A3, A6; :: thesis: verum

end;

end;