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