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

proof

assume b < 0 ; :: thesis: contradiction
then A4: b * 2 < 0 ;
A5: c <= b * 2 by A1;
c < 0 by A1, A4;
then b / c > c / c by A2, Lm32;
then A6: b / c > 1 by A4, A5, XCMPLX_1:60;
then A7: b * (b / c) >= c by A1;
b * (b / c) < c * (b / c) by A2, A6, Lm13;
then b * (b / c) < b by A4, A5, XCMPLX_1:88;
hence contradiction by A2, A7, XXREAL_0:2; :: thesis: verum

end;

per cases ( b > 0 or b = 0 ) by A3;

suppose A8: b > 0 ; :: thesis: contradiction

then b / b < c / b by A2, Lm28;
then 1 < c / b by A8, XCMPLX_1:60;
then consider d being real number such that
A9: ( 1 < d & d < c / b ) by Th7;
b * d < b * (c / b) by A8, A9, Lm13;
then b * d < c by A8, XCMPLX_1:88;
hence contradiction by A1, A9; :: thesis: verum

end;

suppose A10: b = 0 ; :: thesis: contradiction

b * 2 >= c by A1;
hence contradiction by A2, A10; :: thesis: verum

end;

end;