let a, b be Real; :: thesis: a * b <= (1 / 2) * ((a ^2) + (b ^2))
0 <= (a - b) ^2 by XREAL_1:63;
then 0 + ((2 * a) * b) <= (((a ^2) + (b ^2)) - ((2 * a) * b)) + ((2 * a) * b) by XREAL_1:7;
then ((2 * a) * b) / 2 <= ((a ^2) + (b ^2)) / 2 by XREAL_1:72;
hence a * b <= (1 / 2) * ((a ^2) + (b ^2)) ; :: thesis: verum