let b, c be Real; :: thesis: ( ( for a being Real st 1 < a holds
c <= b * a ) implies c <= b )
assume A1: for a being Real st a > 1 holds
b * a >= c ; :: thesis: c <= b
assume A2: not c <= b ; :: thesis: contradiction
A3: b >= 0
proof
A4: c <= b * 2 by A1;
assume b < 0 ; :: thesis: contradiction
then A5: b * 2 < 0 ;
then c < 0 by A1;
then b / c > c / c by A2, Lm29;
then b / c > 1 by A5, A4, XCMPLX_1:60;
then A6: b * (b / c) >= c by A1;
b * (b / c) < c * (b / c) by A2, A5, A4, Lm13;
then b * (b / c) < b by A5, A4, XCMPLX_1:87;
hence contradiction by A2, A6, XXREAL_0:2; :: thesis: verum
end;
per cases ( b > 0 or b = 0 ) by A3;
suppose A7: b > 0 ; :: thesis: contradiction
then b / b < c / b by A2, Lm26;
then 1 < c / b by A7, XCMPLX_1:60;
then consider d being Real such that
A8: 1 < d and
A9: d < c / b by Th5;
b * d < b * (c / b) by A7, A9, Lm13;
then b * d < c by A7, XCMPLX_1:87;
hence contradiction by A1, A8; :: thesis: verum
end;
suppose A10: b = 0 ; :: thesis: contradiction
b * 2 >= c by A1;
hence contradiction by A2, A10; :: thesis: verum
end;
end;