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

proof

assume A1: for a being real number st a > 1 holds
b / a <= c ; :: thesis: b <= c

now

let d be real number ; :: thesis: ( 0 < d & d < 1 implies b <= c / d )
A2: d " = 1 / d by XCMPLX_1:217;
assume A3: ( 0 < d & d < 1 ) ; :: thesis: b <= c / d
then d " > 1 " by Lm39;
then b / (d " ) <= c by A1;
then (b * d) / 1 <= c by A2, XCMPLX_1:78;
hence b <= c / d by A3, Th79; :: thesis: verum

end;

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

end;

hence ( ( for a being real number st 1 < a holds
b / a <= c ) implies b <= c ) ; :: thesis: verum