theorem :: XREAL_1:168

for b, c being Real st ( for a being Real st 0 < a & a < 1 holds
b * a <= c ) holds
b <= c