theorem :: SERIES_5:32

for a, b, c being positive Real holds ((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))