theorem :: XREAL_1:210

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