theorem :: XREAL_1:96

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