let x, y be Real; :: thesis: ( x <= y & x is positive implies y is positive )
assume that
A1: x <= y and
A2: x is positive ; :: thesis: y is positive
x > 0 by A2, XXREAL_0:def 6;
then y > 0 by A1, Lm2;
hence y is positive by XXREAL_0:def 6; :: thesis: verum