theorem SERIES3: :: NUMBER12:61

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