theorem Th66: :: XREAL_1:66

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