theorem :: SERIES_5:33

for a, b, c being positive Real holds ((sqrt (((a ^2) + (b ^2)) / 2)) + (sqrt (((b ^2) + (c ^2)) / 2))) + (sqrt (((c ^2) + (a ^2)) / 2)) <= sqrt (3 * (((a ^2) + (b ^2)) + (c ^2)))