let b, c be Real; :: thesis: ( ( for a being Real st 1 < a holds
b / a <= c ) implies b <= c )
assume A1: for a being Real st a > 1 holds
b / a <= c ; :: thesis: b <= c

now :: thesis: for d being Real st 0 < d & d < 1 holds
b <= c / d

let d be Real; :: thesis: ( 0 < d & d < 1 implies b <= c / d )
A2: d " = 1 / d by XCMPLX_1:215;
assume that
A3: 0 < d and
A4: d < 1 ; :: thesis: b <= c / d
d " > 1 " by A3, A4, Lm34;
then b / (d ") <= c by A1;
then (b * d) / 1 <= c by A2, XCMPLX_1:77;
hence b <= c / d by A3, Th77; :: thesis: verum

end;

hence b <= c by Th209; :: thesis: verum