let x, y be real number ; :: thesis: ( x <= y & not y is zero & not x is negative implies y is positive )
assume A1: ( x <= y & not y is zero & not x is negative & not y is positive ) ; :: thesis: contradiction
then ( x >= 0 & y <= 0 ) by XXREAL_0:def 6, XXREAL_0:def 7;
then ( x >= 0 & y < 0 ) by A1, Lm1;
hence contradiction by A1, Lm2; :: thesis: verum