let x, y, z be real number ; :: thesis: ( (x + y) + z = 1 implies ((x ^2 ) + (y ^2 )) + (z ^2 ) >= 1 / 3 )
assume (x + y) + z = 1 ; :: thesis: ((x ^2 ) + (y ^2 )) + (z ^2 ) >= 1 / 3
then A1: (((((x ^2 ) + (y ^2 )) + (z ^2 )) + ((2 * x) * y)) + ((2 * y) * z)) + ((2 * z) * x) = 1 ^2 by Lm6;
A2: ( ((x ^2 ) + (y ^2 )) / 2 >= x * y & ((y ^2 ) + (z ^2 )) / 2 >= y * z & ((x ^2 ) + (z ^2 )) / 2 >= x * z ) by SERIES_3:7;
then (((x ^2 ) + (y ^2 )) / 2) + (((y ^2 ) + (z ^2 )) / 2) >= (y * z) + (x * y) by XREAL_1:9;
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:9;
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:26;
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:66;
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:8;
then 1 - ((((x ^2 ) + (y ^2 )) + (z ^2 )) * 2) <= 1 - ((((y * z) + (x * y)) + (x * z)) * 2) ;
then 1 <= (((x ^2 ) + (y ^2 )) + (z ^2 )) + ((((x ^2 ) + (y ^2 )) + (z ^2 )) * 2) by A1, XREAL_1:22;
then 1 / 3 <= ((((x ^2 ) + (y ^2 )) + (z ^2 )) * 3) / 3 by XREAL_1:74;
hence ((x ^2 ) + (y ^2 )) + (z ^2 ) >= 1 / 3 ; :: thesis: verum