theorem :: SERIES_5:30

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