theorem :: XREAL_1:97

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