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:65;
A2: a ^2 >= 0 by XREAL_1:65;
then A3: sqrt ((a ^2 ) + (b ^2 )) >= 0 by A1, SQUARE_1:def 4;
(a ^2 ) + (b ^2 ) >= 0 + (a ^2 ) by A1, XREAL_1:9;
then A4: sqrt ((a ^2 ) + (b ^2 )) >= sqrt (a ^2 ) by A2, SQUARE_1:94;

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:89;
then (sqrt ((a ^2 ) + (b ^2 ))) - a >= a - a by XREAL_1:11;
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:90;
then (sqrt ((a ^2 ) + (b ^2 ))) - (- a) >= (- a) - (- a) by XREAL_1:11;
hence ( ((- a) + (sqrt ((a ^2 ) + (b ^2 )))) / 2 >= 0 & (a + (sqrt ((a ^2 ) + (b ^2 )))) / 2 >= 0 ) by A3, A6; :: thesis: verum

end;

end;