let x, y be Real; :: thesis: ((x ^2) + (y ^2)) / 2 >= ((x + y) / 2) ^2
(x - y) ^2 >= 0 by XREAL_1:63;
then (((x ^2) - ((2 * x) * y)) + (y ^2)) + ((2 * x) * y) >= 0 + ((2 * x) * y) by XREAL_1:7;
then ((x ^2) + (y ^2)) + ((x ^2) + (y ^2)) >= ((2 * x) * y) + ((x ^2) + (y ^2)) by XREAL_1:7;
then (2 * ((x ^2) + (y ^2))) / 4 >= ((x + y) ^2) / 4 by XREAL_1:72;
hence ((x ^2) + (y ^2)) / 2 >= ((x + y) / 2) ^2 ; :: thesis: verum