theorem SRI: :: COMPLEX3:48
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