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