let x, y be real number ; :: thesis: ((x ^2 ) + (y ^2 )) / 2 >= ((x + y) / 2) ^2
(x - y) ^2 >= 0 by XREAL_1:65;
then (((x ^2 ) - ((2 * x) * y)) + (y ^2 )) + ((2 * x) * y) >= 0 + ((2 * x) * y) by XREAL_1:9;
then ((x ^2 ) + (y ^2 )) + ((x ^2 ) + (y ^2 )) >= ((2 * x) * y) + ((x ^2 ) + (y ^2 )) by XREAL_1:9;
then (2 * ((x ^2 ) + (y ^2 ))) / 4 >= ((x + y) ^2 ) / 4 by XREAL_1:74;
hence ((x ^2 ) + (y ^2 )) / 2 >= ((x + y) / 2) ^2 ; :: thesis: verum