let x, y be real number ; :: thesis: x + y <= sqrt (2 * ((x ^2 ) + (y ^2 )))
(x ^2 ) + (y ^2 ) >= (2 * x) * y by SERIES_3:6;
then A1: ((x ^2 ) + (y ^2 )) + ((x ^2 ) + (y ^2 )) >= ((2 * x) * y) + ((x ^2 ) + (y ^2 )) by XREAL_1:8;
then A2: 2 * ((x ^2 ) + (y ^2 )) >= (x + y) ^2 ;
A3: (x + y) ^2 >= 0 by XREAL_1:65;
then A4: sqrt (2 * ((x ^2 ) + (y ^2 ))) >= sqrt ((x + y) ^2 ) by A1, SQUARE_1:94;

per cases ( x + y > 0 or x + y = 0 or x + y < 0 ) ;

suppose x + y > 0 ; :: thesis: x + y <= sqrt (2 * ((x ^2 ) + (y ^2 )))

hence x + y <= sqrt (2 * ((x ^2 ) + (y ^2 ))) by A4, SQUARE_1:89; :: thesis: verum

end;

suppose x + y = 0 ; :: thesis: x + y <= sqrt (2 * ((x ^2 ) + (y ^2 )))

hence x + y <= sqrt (2 * ((x ^2 ) + (y ^2 ))) by A2, SQUARE_1:82, SQUARE_1:94; :: thesis: verum

end;

suppose x + y < 0 ; :: thesis: x + y <= sqrt (2 * ((x ^2 ) + (y ^2 )))

hence x + y <= sqrt (2 * ((x ^2 ) + (y ^2 ))) by A1, A3, SQUARE_1:def 4; :: thesis: verum

end;

end;