let x, y, z be Real; :: thesis: ( (x + y) + z = 1 implies ((x * y) + (y * z)) + (x * z) <= 1 / 3 )
( (x ^2) + (y ^2) >= (2 * x) * y & (x ^2) + (z ^2) >= (2 * x) * z ) by Th6;
then A1: ((x ^2) + (y ^2)) + ((x ^2) + (z ^2)) >= ((2 * x) * y) + ((2 * x) * z) by XREAL_1:7;
(y ^2) + (z ^2) >= (2 * y) * z by Th6;
then ((((x ^2) + (y ^2)) + (x ^2)) + (z ^2)) + ((y ^2) + (z ^2)) >= (((2 * x) * y) + ((2 * x) * z)) + ((2 * y) * z) by A1, XREAL_1:7;
then (2 * (((x ^2) + (y ^2)) + (z ^2))) / 2 >= (2 * (((x * y) + (x * z)) + (y * z))) / 2 by XREAL_1:72;
then A2: (((x ^2) + (y ^2)) + (z ^2)) + (2 * (((x * z) + (y * z)) + (x * y))) >= (((x * y) + (x * z)) + (y * z)) + (2 * (((x * z) + (y * z)) + (x * y))) by XREAL_1:7;
assume (x + y) + z = 1 ; :: thesis: ((x * y) + (y * z)) + (x * z) <= 1 / 3
then 1 ^2 = (((x + y) ^2) + ((2 * (x + y)) * z)) + (z ^2) by SQUARE_1:4
.= (((x ^2) + (y ^2)) + (z ^2)) + (2 * (((x * z) + (y * z)) + (x * y))) ;
then 1 / 3 >= (3 * (((x * z) + (y * z)) + (x * y))) / 3 by A2, XREAL_1:72;
hence ((x * y) + (y * z)) + (x * z) <= 1 / 3 ; :: thesis: verum