let x, y, z be real number ; :: thesis: ((x ^2 ) + (y ^2 )) + (z ^2 ) >= ((x * y) + (y * z)) + (x * z)
A1: (x ^2 ) + (y ^2 ) >= (2 * x) * y by Th6;
A2: (y ^2 ) + (z ^2 ) >= (2 * y) * z by Th6;
A3: (z ^2 ) + (x ^2 ) >= (2 * z) * x by Th6;
((x ^2 ) + (y ^2 )) + ((y ^2 ) + (z ^2 )) >= ((2 * x) * y) + ((2 * y) * z) by A1, A2, XREAL_1:9;
then (((x ^2 ) + (y ^2 )) + ((y ^2 ) + (z ^2 ))) + ((z ^2 ) + (x ^2 )) >= (((2 * x) * y) + ((2 * y) * z)) + ((2 * z) * x) by A3, 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