let x, y, z be real number ; :: 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:9;
(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:9;
then (2 * (((x ^2 ) + (y ^2 )) + (z ^2 ))) / 2 >= (2 * (((x * y) + (y * z)) + (z * x))) / 2 by XREAL_1:74;
hence ((x ^2 ) + (y ^2 )) + (z ^2 ) >= ((x * y) + (y * z)) + (x * z) ; :: thesis: verum