let a, b, c be real positive number ; :: thesis: ((sqrt ((((a ^2 ) + (a * b)) + (b ^2 )) / 3)) + (sqrt ((((b ^2 ) + (b * c)) + (c ^2 )) / 3))) + (sqrt ((((c ^2 ) + (c * a)) + (a ^2 )) / 3)) <= ((sqrt (((a ^2 ) + (b ^2 )) / 2)) + (sqrt (((b ^2 ) + (c ^2 )) / 2))) + (sqrt (((c ^2 ) + (a ^2 )) / 2))
A1: sqrt ((((a ^2 ) + (a * b)) + (b ^2 )) / 3) <= sqrt (((a ^2 ) + (b ^2 )) / 2) by Lm12;
sqrt ((((b ^2 ) + (b * c)) + (c ^2 )) / 3) <= sqrt (((b ^2 ) + (c ^2 )) / 2) by Lm12;
then A2: (sqrt ((((a ^2 ) + (a * b)) + (b ^2 )) / 3)) + (sqrt ((((b ^2 ) + (b * c)) + (c ^2 )) / 3)) <= (sqrt (((a ^2 ) + (b ^2 )) / 2)) + (sqrt (((b ^2 ) + (c ^2 )) / 2)) by A1, XREAL_1:9;
sqrt ((((c ^2 ) + (c * a)) + (a ^2 )) / 3) <= sqrt (((c ^2 ) + (a ^2 )) / 2) by Lm12;
hence ((sqrt ((((a ^2 ) + (a * b)) + (b ^2 )) / 3)) + (sqrt ((((b ^2 ) + (b * c)) + (c ^2 )) / 3))) + (sqrt ((((c ^2 ) + (c * a)) + (a ^2 )) / 3)) <= ((sqrt (((a ^2 ) + (b ^2 )) / 2)) + (sqrt (((b ^2 ) + (c ^2 )) / 2))) + (sqrt (((c ^2 ) + (a ^2 )) / 2)) by A2, XREAL_1:9; :: thesis: verum