theorem :: XREAL_1:64

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