let a, b, c be positive Real; :: 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 ((((b ^2) + (b * c)) + (c ^2)) / 3) <= sqrt (((b ^2) + (c ^2)) / 2) by Lm12;
A2: sqrt ((((c ^2) + (c * a)) + (a ^2)) / 3) <= sqrt (((c ^2) + (a ^2)) / 2) by Lm12;
sqrt ((((a ^2) + (a * b)) + (b ^2)) / 3) <= sqrt (((a ^2) + (b ^2)) / 2) by Lm12;
then (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:7;
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:7; :: thesis: verum