let x, y be Real; :: thesis: ((x ^2) + (y ^2)) / 2 >= x * y
((x ^2) + (y ^2)) / 2 >= ((2 * x) * y) / 2 by Th6, XREAL_1:72;
hence ((x ^2) + (y ^2)) / 2 >= x * y ; :: thesis: verum