let x, y, z be Real; :: thesis: ((x + y) + z) ^2 >= 3 * (((x * y) + (y * z)) + (x * z))
((x ^2) + (y ^2)) + (z ^2) >= ((x * y) + (y * z)) + (x * z) by Th10;
then (((x ^2) + (y ^2)) + (z ^2)) + ((((2 * x) * y) + ((2 * y) * z)) + ((2 * z) * x)) >= (((x * y) + (y * z)) + (x * z)) + ((((2 * x) * y) + ((2 * y) * z)) + ((2 * z) * x)) by XREAL_1:6;
hence ((x + y) + z) ^2 >= 3 * (((x * y) + (y * z)) + (x * z)) ; :: thesis: verum