let b, c be real number ; :: thesis: ( ( for a being real number st 0 < a & a < 1 holds
b <= a * c ) implies b <= 0 )
assume that
A1: for a being real number st 0 < a & a < 1 holds
b <= a * c and
A2: b > 0 ; :: thesis: contradiction
A3: b * 2 > b by A2, Th157;
then A4: b > b / 2 by Th85;

per cases ( c <= 0 or ( c <= b & c > 0 ) or ( b <= c & c > 0 ) ) ;

suppose c <= 0 ; :: thesis: contradiction

then (1 / 2) * c <= 0 ;
hence contradiction by A1, A2; :: thesis: verum

end;

suppose that A5: c <= b and
A6: c > 0 ; :: thesis: contradiction

set a = c / (2 * b);
A7: 2 * b > 0 by A2;
A8: c / b <= 1 by A5, A6, Lm47;
(c / b) * 2 > c / b by A2, A6, Th157;
then c / b > (c / b) / 2 by Th85;
then c / b > c / (b * 2) by XCMPLX_1:79;
then c / (2 * b) < 1 by A8, XXREAL_0:2;
then A9: (c / (2 * b)) * c >= b by A1, A6, A7;

per cases ( c >= b or c < b ) ;

suppose c >= b ; :: thesis: contradiction

then b = c by A5, XXREAL_0:1;
then (c / (2 * b)) * c = b / 2 by A6, XCMPLX_1:93;
hence contradiction by A2, A9, Th85, Th157; :: thesis: verum

end;

suppose A10: c < b ; :: thesis: contradiction

(c / (2 * b)) * c < (c / (2 * b)) * b by A6, A10, Th100;
then A11: (c / (2 * b)) * c < c / 2 by A2, XCMPLX_1:93;
c / 2 < b / 2 by A10, Lm28;
then (c / (2 * b)) * c < b / 2 by A11, XXREAL_0:2;
hence contradiction by A4, A9, XXREAL_0:2; :: thesis: verum

end;

end;

end;

suppose that A12: b <= c and
A13: c > 0 ; :: thesis: contradiction

set a = b / (2 * c);
A14: 2 * c > 0 by A13;
A15: b / c <= 1 by A12, A13, Lm48;
(b / c) * 2 > b / c by A2, A13, Th157;
then b / c > (b / c) / 2 by Th85;
then b / c > b / (c * 2) by XCMPLX_1:79;
then b / (2 * c) < 1 by A15, XXREAL_0:2;
then A16: (b / (2 * c)) * c >= b by A1, A2, A14;
(b / (2 * c)) * c = b / 2 by A13, XCMPLX_1:93;
hence contradiction by A3, A16, Th85; :: thesis: verum

end;

end;