let x, y be Real; :: thesis: (x ^2) + (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:6;
hence (x ^2) + (y ^2) >= (2 * x) * y ; :: thesis: verum