theorem Th167: :: XREAL_1:167

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