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

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);
(c / b) * 2 > c / b by A2, A6, Th155;
then c / b > (c / b) / 2 by Th83;
then A7: c / b > c / (b * 2) by XCMPLX_1:78;
c / b <= 1 by A5, A6, Lm37;
then c / (2 * b) < 1 by A7, XXREAL_0:2;
then A8: (c / (2 * b)) * c >= b by A1, A2, A6;

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:92;
hence contradiction by A2, A8, Th83, Th155; :: thesis: verum

end;

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

then (c / (2 * b)) * c < (c / (2 * b)) * b by A6, Th98;
then A10: (c / (2 * b)) * c < c / 2 by A2, XCMPLX_1:92;
c / 2 < b / 2 by A9, Lm26;
then (c / (2 * b)) * c < b / 2 by A10, XXREAL_0:2;
hence contradiction by A4, A8, XXREAL_0:2; :: thesis: verum

end;

end;

end;

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

set a = b / (2 * c);
(b / c) * 2 > b / c by A2, A12, Th155;
then b / c > (b / c) / 2 by Th83;
then A13: b / c > b / (c * 2) by XCMPLX_1:78;
b / c <= 1 by A11, A12, Lm38;
then b / (2 * c) < 1 by A13, XXREAL_0:2;
then A14: (b / (2 * c)) * c >= b by A1, A2, A12;
(b / (2 * c)) * c = b / 2 by A12, XCMPLX_1:92;
hence contradiction by A3, A14, Th83; :: thesis: verum

end;

end;