let x, y, z be Real; :: thesis: ( (x + y) + z = 1 implies ((x * y) + (y * z)) + (z * x) <= 1 / 3 )
((x ^2) + (y ^2)) + (z ^2) >= ((x * y) + (y * z)) + (x * z) by SERIES_3:10;
then A1: (((x ^2) + (y ^2)) + (z ^2)) + (2 * (((x * y) + (y * z)) + (z * x))) >= (((x * y) + (y * z)) + (x * z)) + (2 * (((x * y) + (y * z)) + (z * x))) by XREAL_1:7;
assume (x + y) + z = 1 ; :: thesis: ((x * y) + (y * z)) + (z * x) <= 1 / 3
then 1 ^2 = (((((x ^2) + (y ^2)) + (z ^2)) + ((2 * x) * y)) + ((2 * y) * z)) + ((2 * z) * x) by Lm6;
then 1 / 3 >= (3 * (((x * y) + (y * z)) + (z * x))) / 3 by A1, XREAL_1:72;
hence ((x * y) + (y * z)) + (z * x) <= 1 / 3 ; :: thesis: verum