theorem :: XREAL_1:100
for a, b, c being Real st c < 0 & 0 < a & a < b holds
c / a < c / b