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