theorem :: COMPLEX3:47

for a, b, c, d being positive Real st a * b < c * d & (1 / a) + (1 / b) <= (1 / c) + (1 / d) holds
a + b < c + d by SRL;