theorem :: SERIES_5:34

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