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