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

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

let d be Real; :: thesis: ( d > 1 implies b * d >= c )
assume d > 1 ; :: thesis: b * d >= c
then A2: b / (d ") >= c by A1, Lm36;
d " = 1 / d by XCMPLX_1:215;
then (b * d) / 1 >= c by A2, XCMPLX_1:77;
hence b * d >= c ; :: thesis: verum

end;

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