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

now

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

end;

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