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

now :: thesis: for d being Real st d > 1 holds
b <= c * d

let d be Real; :: thesis: ( d > 1 implies b <= c * d )
assume A2: d > 1 ; :: thesis: b <= c * d
then b * (d ") <= c by A1, Lm36;
then b / d <= c by XCMPLX_0:def 9;
hence b <= c * d by A2, Th81; :: thesis: verum

end;

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