let x, y be ext-real number ; :: thesis: ( x <= 0 & y < 0 implies x + y < 0 )
assume x <= 0 ; :: thesis: ( not y < 0 or x + y < 0 )
then x + y <= 0 + y by Lm5E;
hence ( not y < 0 or x + y < 0 ) by Tx3; :: thesis: verum