theorem :: SERIES_3:16

for a, b, c being positive Real holds ((a + b) + c) / 3 >= 3 -root ((a * b) * c)