theorem Th54: :: NUMBER09:54
for a, b, c, d being positive Real st a / b < 1 & c / d < 1 holds
(a / b) * (c / d) < 1