let x, y be real number ; :: thesis: ( ( for c being real number st c > 0 & c < 1 holds
c * x >= y ) implies y <= 0 )
assume A1: for c being real number st c > 0 & c < 1 holds
c * x >= y ; :: thesis: y <= 0
assume A2: y > 0 ; :: thesis: contradiction
set mi = min x,y;
set ma = max x,y;
set c = (min x,y) / (2 * (max x,y));
A3: y * 2 > y by A2, XREAL_1:157;

per cases ( x > 0 or x <= 0 ) ;

suppose A4: x > 0 ; :: thesis: contradiction

then A5: ( min x,y > 0 & max x,y > 0 ) by A2, XXREAL_0:15, XXREAL_0:16;
A6: (min x,y) / (2 * (max x,y)) > 0 by A5;
A7: (min x,y) / (max x,y) <= 1 by A4, Th2;
((min x,y) / (max x,y)) * 2 > (min x,y) / (max x,y) by A5, XREAL_1:157;
then (min x,y) / (max x,y) > ((min x,y) / (max x,y)) / 2 by XREAL_1:85;
then (min x,y) / (max x,y) > (min x,y) / ((max x,y) * 2) by XCMPLX_1:79;
then (min x,y) / (2 * (max x,y)) < 1 by A7, XXREAL_0:2;
then A8: ((min x,y) / (2 * (max x,y))) * x >= y by A1, A6;

now

per cases ( x >= y or x < y ) ;

suppose x >= y ; :: thesis: contradiction

then ( max x,y = x & min x,y = y ) by XXREAL_0:def 9, XXREAL_0:def 10;
then ((min x,y) / (2 * (max x,y))) * x = y / 2 by A4, XCMPLX_1:93;
hence contradiction by A3, A8, XREAL_1:85; :: thesis: verum

end;

suppose A9: x < y ; :: thesis: contradiction

then A10: ( max x,y = y & min x,y = x ) by XXREAL_0:def 9, XXREAL_0:def 10;
((min x,y) / (2 * (max x,y))) * x < (x / (2 * y)) * y by A4, A9, A10, XREAL_1:100;
then A11: ((min x,y) / (2 * (max x,y))) * x < x / 2 by A2, XCMPLX_1:93;
x / 2 < y / 2 by A9, XREAL_1:76;
then A12: ((min x,y) / (2 * (max x,y))) * x < y / 2 by A11, XXREAL_0:2;
y > y / 2 by A3, XREAL_1:85;
hence contradiction by A8, A12, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence contradiction ; :: thesis: verum

end;

suppose x <= 0 ; :: thesis: contradiction

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

end;

end;