let x, y be Real; :: thesis: ( x <= y & not y is zero & not x is negative implies y is positive )
assume that
A1: x <= y and
A2: not y is zero and
A3: not x is negative and
A4: not y is positive ; :: thesis: contradiction
y <= 0 by A4, XXREAL_0:def 6;
then A5: y < 0 by A2, Lm1;
x >= 0 by A3, XXREAL_0:def 7;
hence contradiction by A1, A5, Lm2; :: thesis: verum