theorem SIL: :: COMPLEX3:33

for a, b being positive Real holds
( a + b > a * b iff (1 / a) + (1 / b) > 1 )