theorem :: SERIES_5:42

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