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

assume that

A1: x <= y and

A2: not x is zero and

A3: not y is positive and

A4: not x is negative ; :: thesis: contradiction

x >= 0 by A4, XXREAL_0:def 7;

then A5: x > 0 by A2, Lm1;

y <= 0 by A3, XXREAL_0:def 6;

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

assume that

A1: x <= y and

A2: not x is zero and

A3: not y is positive and

A4: not x is negative ; :: thesis: contradiction

x >= 0 by A4, XXREAL_0:def 7;

then A5: x > 0 by A2, Lm1;

y <= 0 by A3, XXREAL_0:def 6;

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