theorem :: SERIES_5:2

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