theorem Th209: :: XREAL_1:209

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