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
set ma = max x,y;
set mi = min x,y;
set c = (min x,y) / (2 * (max x,y));
assume A2: y > 0 ; :: thesis: contradiction
then A3: y * 2 > y by 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;
then ((min x,y) / (max x,y)) * 2 > (min x,y) / (max x,y) by XREAL_1:157;
then (min x,y) / (max x,y) > ((min x,y) / (max x,y)) / 2 by XREAL_1:85;
then A6: (min x,y) / (max x,y) > (min x,y) / ((max x,y) * 2) by XCMPLX_1:79;
(min x,y) / (max x,y) <= 1 by A4, Th2;
then (min x,y) / (2 * (max x,y)) < 1 by A6, XXREAL_0:2;
then A7: ((min x,y) / (2 * (max x,y))) * x >= y by A1, A5;

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, A7, XREAL_1:85; :: thesis: verum

end;

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

then ( max x,y = y & min x,y = x ) by XXREAL_0:def 9, XXREAL_0:def 10;
then ((min x,y) / (2 * (max x,y))) * x < (x / (2 * y)) * y by A4, A8, XREAL_1:100;
then A9: ((min x,y) / (2 * (max x,y))) * x < x / 2 by A2, XCMPLX_1:93;
A10: y > y / 2 by A3, XREAL_1:85;
x / 2 < y / 2 by A8, XREAL_1:76;
then ((min x,y) / (2 * (max x,y))) * x < y / 2 by A9, XXREAL_0:2;
hence contradiction by A7, A10, 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;