let x, y be real number ; :: thesis: (x + y) ^2 >= (4 * x) * y
2 * (((x ^2 ) + (y ^2 )) / 2) >= 2 * (x * y) by Th7, XREAL_1:66;
then ((x ^2 ) + (y ^2 )) + ((2 * x) * y) >= ((2 * x) * y) + ((2 * x) * y) by XREAL_1:8;
hence (x + y) ^2 >= (4 * x) * y ; :: thesis: verum