theorem :: SERIES_3:27

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