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

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