let a, b be positive Real; :: thesis: (a + b) / 2 <= sqrt (((a ^2) + (b ^2)) / 2)
(a ^2) + (b ^2) >= (2 * a) * b by SERIES_3:6;
then ((a ^2) + (b ^2)) + ((a ^2) + (b ^2)) >= ((2 * a) * b) + ((a ^2) + (b ^2)) by XREAL_1:7;
then sqrt (2 * ((a ^2) + (b ^2))) >= sqrt ((a + b) ^2) by SQUARE_1:26;
then sqrt (2 * ((a ^2) + (b ^2))) >= a + b by SQUARE_1:22;
then (sqrt (2 * ((a ^2) + (b ^2)))) / (sqrt (2 * 2)) >= (a + b) / 2 by SQUARE_1:20, XREAL_1:72;
then (sqrt (2 * ((a ^2) + (b ^2)))) / ((sqrt 2) * (sqrt 2)) >= (a + b) / 2 by SQUARE_1:29;
then ((sqrt 2) * (sqrt ((a ^2) + (b ^2)))) / ((sqrt 2) * (sqrt 2)) >= (a + b) / 2 by SQUARE_1:29;
then A1: (((sqrt 2) / (sqrt 2)) * (sqrt ((a ^2) + (b ^2)))) / (sqrt 2) >= (a + b) / 2 by XCMPLX_1:83;
sqrt 2 > 0 by SQUARE_1:25;
then (1 * (sqrt ((a ^2) + (b ^2)))) / (sqrt 2) >= (a + b) / 2 by A1, XCMPLX_1:60;
hence (a + b) / 2 <= sqrt (((a ^2) + (b ^2)) / 2) by SQUARE_1:30; :: thesis: verum