let x, y be Real; :: 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:6;
then A2: 2 * ((x ^2) + (y ^2)) >= (x + y) ^2 ;
A3: (x + y) ^2 >= 0 by XREAL_1:63;
then A4: sqrt (2 * ((x ^2) + (y ^2))) >= sqrt ((x + y) ^2) by A1, SQUARE_1:26;

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:22; :: 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:17, SQUARE_1:26; :: 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 2; :: thesis: verum

end;

end;