theorem :: SERIES_3:30

for a, b, c being positive Real st a >= b & b >= c holds
((a to_power a) * (b to_power b)) * (c to_power c) >= ((a * b) * c) to_power (((a + b) + c) / 3)