theorem Th98: :: XREAL_1:98

for a, b, c, d being Real st 0 < a & 0 < c & a <= b & c < d holds
a * c < b * d