theorem :: XREAL_1:169

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