let x, y be Real; :: thesis: (x + y) ^2 >= (4 * x) * y
2 * (((x ^2) + (y ^2)) / 2) >= 2 * (x * y) by Th7, XREAL_1:64;
then ((x ^2) + (y ^2)) + ((2 * x) * y) >= ((2 * x) * y) + ((2 * x) * y) by XREAL_1:6;
hence (x + y) ^2 >= (4 * x) * y ; :: thesis: verum