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