let x, y be Real; :: thesis: ( not x <= y & not y is negative implies x is positive )

assume that

A1: x > y and

A2: ( not y is negative & not x is positive ) ; :: 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 y is negative & not x is positive ) ; :: thesis: contradiction

( x <= 0 & y >= 0 ) by A2, XXREAL_0:def 6, XXREAL_0:def 7;

hence contradiction by A1, Lm2; :: thesis: verum