theorem :: SERIES_5:37
for a, b, c being positive Real st (a + b) + c = 1 holds
((1 / a) + (1 / b)) + (1 / c) >= 9