theorem :: XREAL_1:68

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