let x, y be real number ; :: thesis: ( x <= y & not x is negative implies not y is negative )
assume A1: ( x <= y & not x is negative & y is negative ) ; :: thesis: contradiction
then y < 0 by XXREAL_0:def 7;
then x < 0 by A1, Lm2;
hence contradiction by A1, XXREAL_0:def 7; :: thesis: verum