let x, y be Real; :: thesis: ((x + y) / 2) ^2 >= x * y
(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)) + ((2 * x) * y) >= ((2 * x) * y) + ((2 * x) * y) by XREAL_1:7;
then ((x + y) ^2) / (2 * 2) >= (4 * (x * y)) / 4 by XREAL_1:72;
hence ((x + y) / 2) ^2 >= x * y ; :: thesis: verum