let a, b, c be positive Real; (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 3 > 0
by SQUARE_1:25;
A2:
sqrt (((c ^2) + (c * a)) + (a ^2)) >= ((1 / 2) * (sqrt 3)) * (c + a)
by Lm11;
A3:
sqrt (((b ^2) + (b * c)) + (c ^2)) >= ((1 / 2) * (sqrt 3)) * (b + c)
by Lm11;
sqrt (((a ^2) + (a * b)) + (b ^2)) >= ((1 / 2) * (sqrt 3)) * (a + b)
by Lm11;
then
(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 A3, XREAL_1:7;
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:7;
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 A1, XREAL_1:72;
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: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) * 1
by A1, 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:62;
then
(((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:62;
then
((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 SQUARE_1:30;
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:30;
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:30; verum