theorem :: XREAL_1:69

for a, b, c being Real st c < 0 & a < b holds
b * c < a * c by Lm24;