let x, y be ExtReal; :: 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 Lm12;
hence ( not y < 0 or x + y < 0 ) by Th4; :: thesis: verum