theorem :: SERIES_3:20

for a, b being positive Real st a + b = 1 holds
(1 + (1 / a)) * (1 + (1 / b)) >= 9