let a, b be Real; :: thesis: ( ((- a) + (sqrt ((a ^2 ) + (b ^2 )))) / 2 >= 0 & (a + (sqrt ((a ^2 ) + (b ^2 )))) / 2 >= 0 )
A1: ( a ^2 >= 0 & b ^2 >= 0 & a ^2 >= a ^2 ) by XREAL_1:65;
then ( (a ^2 ) + (b ^2 ) >= 0 + 0 & (a ^2 ) + (b ^2 ) >= 0 + (a ^2 ) ) by XREAL_1:9;
then A3: sqrt ((a ^2 ) + (b ^2 )) >= sqrt (a ^2 ) by A1, SQUARE_1:94;
A4: sqrt ((a ^2 ) + (b ^2 )) >= 0 by A1, SQUARE_1:def 4;

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

suppose B5: 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 & a + (sqrt ((a ^2 ) + (b ^2 ))) >= 0 + 0 ) by A3, 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 B5, A4; :: thesis: verum

end;

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

( sqrt ((a ^2 ) + (b ^2 )) >= - a & (- a) + (sqrt ((a ^2 ) + (b ^2 ))) >= 0 + 0 ) by A3, A4, A6, 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 A4, A6; :: thesis: verum

end;

end;