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

assume that

A1: x <= y and

A2: not y is positive and

A3: x is positive ; :: thesis: contradiction

x > 0 by A3, XXREAL_0:def 6;

then y > 0 by A1, Lm2;

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

assume that

A1: x <= y and

A2: not y is positive and

A3: x is positive ; :: thesis: contradiction

x > 0 by A3, XXREAL_0:def 6;

then y > 0 by A1, Lm2;

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