let x, y, z be Real; :: thesis: ((x ^2) + (y ^2)) + (z ^2) >= ((x * y) + (y * z)) + (x * z)
( (x ^2) + (y ^2) >= (2 * x) * y & (y ^2) + (z ^2) >= (2 * y) * z ) by Th6;
then A1: ((x ^2) + (y ^2)) + ((y ^2) + (z ^2)) >= ((2 * x) * y) + ((2 * y) * z) by XREAL_1:7;
(z ^2) + (x ^2) >= (2 * z) * x by Th6;
then (((x ^2) + (y ^2)) + ((y ^2) + (z ^2))) + ((z ^2) + (x ^2)) >= (((2 * x) * y) + ((2 * y) * z)) + ((2 * z) * x) by A1, XREAL_1:7;
then (2 * (((x ^2) + (y ^2)) + (z ^2))) / 2 >= (2 * (((x * y) + (y * z)) + (z * x))) / 2 by XREAL_1:72;
hence ((x ^2) + (y ^2)) + (z ^2) >= ((x * y) + (y * z)) + (x * z) ; :: thesis: verum