let x, y be real number ; :: thesis: (x ^2 ) + (y ^2 ) >= (2 * x) * y
(x - y) ^2 >= 0 by XREAL_1:65;
then (((x ^2 ) - ((2 * x) * y)) + (y ^2 )) + ((2 * x) * y) >= 0 + ((2 * x) * y) by XREAL_1:8;
hence (x ^2 ) + (y ^2 ) >= (2 * x) * y ; :: thesis: verum