theorem Th13: :: SERIES_3:13

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