let x, y be Real; :: thesis: ( ( for c being Real st c > 0 & c < 1 holds
c * x >= y ) implies y <= 0 )
assume A1: for c being Real 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:155;
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:155;
then (min (x,y)) / (max (x,y)) > ((min (x,y)) / (max (x,y))) / 2 by XREAL_1:83;
then A6: (min (x,y)) / (max (x,y)) > (min (x,y)) / ((max (x,y)) * 2) by XCMPLX_1:78;
(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 :: thesis: contradiction
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:92;
hence contradiction by A3, A7, XREAL_1:83; :: 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:98;
then A9: ((min (x,y)) / (2 * (max (x,y)))) * x < x / 2 by A2, XCMPLX_1:92;
A10: y > y / 2 by A3, XREAL_1:83;
x / 2 < y / 2 by A8, XREAL_1:74;
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;