theorem :: XREAL_1:70

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