let b, c be real number ; :: thesis: ( ( for a being real number st 0 < a & a < 1 holds
b * a <= c ) implies b <= c )
assume A1: for a being real number st 0 < a & a < 1 holds
b * a <= c ; :: thesis: b <= c

now

let d be real number ; :: thesis: ( d > 1 implies b <= c * d )
assume A3: d > 1 ; :: thesis: b <= c * d
then ( 0 < d " & d " < 1 ) by Lm46;
then b * (d " ) <= c by A1;
then b / d <= c by XCMPLX_0:def 9;
hence b <= c * d by A3, Th83; :: thesis: verum

end;

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