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

assume that

A1: x <= y and

A2: not x is negative and

A3: y is negative ; :: thesis: contradiction

y < 0 by A3, XXREAL_0:def 7;

then x < 0 by A1, Lm2;

hence contradiction by A2, XXREAL_0:def 7; :: thesis: verum

assume that

A1: x <= y and

A2: not x is negative and

A3: y is negative ; :: thesis: contradiction

y < 0 by A3, XXREAL_0:def 7;

then x < 0 by A1, Lm2;

hence contradiction by A2, XXREAL_0:def 7; :: thesis: verum