let a, b, c be real positive number ; :: thesis: (a + b) + c <= ((sqrt ((((a ^2 ) + (a * b)) + (b ^2 )) / 3)) + (sqrt ((((b ^2 ) + (b * c)) + (c ^2 )) / 3))) + (sqrt ((((c ^2 ) + (c * a)) + (a ^2 )) / 3))
A1: sqrt (((a ^2 ) + (a * b)) + (b ^2 )) >= ((1 / 2) * (sqrt 3)) * (a + b) by Lm11;
sqrt (((b ^2 ) + (b * c)) + (c ^2 )) >= ((1 / 2) * (sqrt 3)) * (b + c) by Lm11;
then A2: (sqrt (((a ^2 ) + (a * b)) + (b ^2 ))) + (sqrt (((b ^2 ) + (b * c)) + (c ^2 ))) >= (((1 / 2) * (sqrt 3)) * (a + b)) + (((1 / 2) * (sqrt 3)) * (b + c)) by A1, XREAL_1:9;
A3: sqrt 3 > 0 by SQUARE_1:93;
sqrt (((c ^2 ) + (c * a)) + (a ^2 )) >= ((1 / 2) * (sqrt 3)) * (c + a) by Lm11;
then ((sqrt (((a ^2 ) + (a * b)) + (b ^2 ))) + (sqrt (((b ^2 ) + (b * c)) + (c ^2 )))) + (sqrt (((c ^2 ) + (c * a)) + (a ^2 ))) >= ((((1 / 2) * (sqrt 3)) * (a + b)) + (((1 / 2) * (sqrt 3)) * (b + c))) + (((1 / 2) * (sqrt 3)) * (c + a)) by A2, XREAL_1:9;
then (((sqrt (((a ^2 ) + (a * b)) + (b ^2 ))) + (sqrt (((b ^2 ) + (b * c)) + (c ^2 )))) + (sqrt (((c ^2 ) + (c * a)) + (a ^2 )))) / (sqrt 3) >= (((a + b) + c) * (sqrt 3)) / (sqrt 3) by A3, XREAL_1:74;
then (((sqrt (((a ^2 ) + (a * b)) + (b ^2 ))) + (sqrt (((b ^2 ) + (b * c)) + (c ^2 )))) + (sqrt (((c ^2 ) + (c * a)) + (a ^2 )))) / (sqrt 3) >= ((a + b) + c) * ((sqrt 3) / (sqrt 3)) by XCMPLX_1:75;
then (((sqrt (((a ^2 ) + (a * b)) + (b ^2 ))) + (sqrt (((b ^2 ) + (b * c)) + (c ^2 )))) + (sqrt (((c ^2 ) + (c * a)) + (a ^2 )))) / (sqrt 3) >= ((a + b) + c) * 1 by A3, XCMPLX_1:60;
then (((sqrt (((a ^2 ) + (a * b)) + (b ^2 ))) + (sqrt (((b ^2 ) + (b * c)) + (c ^2 )))) / (sqrt 3)) + ((sqrt (((c ^2 ) + (c * a)) + (a ^2 ))) / (sqrt 3)) >= (a + b) + c by XCMPLX_1:63;
then A4: (((sqrt (((a ^2 ) + (a * b)) + (b ^2 ))) / (sqrt 3)) + ((sqrt (((b ^2 ) + (b * c)) + (c ^2 ))) / (sqrt 3))) + ((sqrt (((c ^2 ) + (c * a)) + (a ^2 ))) / (sqrt 3)) >= (a + b) + c by XCMPLX_1:63;
((sqrt ((((a ^2 ) + (a * b)) + (b ^2 )) / 3)) + ((sqrt (((b ^2 ) + (b * c)) + (c ^2 ))) / (sqrt 3))) + ((sqrt (((c ^2 ) + (c * a)) + (a ^2 ))) / (sqrt 3)) >= (a + b) + c by A4, SQUARE_1:99;
then ((sqrt ((((a ^2 ) + (a * b)) + (b ^2 )) / 3)) + (sqrt ((((b ^2 ) + (b * c)) + (c ^2 )) / 3))) + ((sqrt (((c ^2 ) + (c * a)) + (a ^2 ))) / (sqrt 3)) >= (a + b) + c by SQUARE_1:99;
hence (a + b) + c <= ((sqrt ((((a ^2 ) + (a * b)) + (b ^2 )) / 3)) + (sqrt ((((b ^2 ) + (b * c)) + (c ^2 )) / 3))) + (sqrt ((((c ^2 ) + (c * a)) + (a ^2 )) / 3)) by SQUARE_1:99; :: thesis: verum