theorem :: SERIES_3:29

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