let r, s be Real; :: thesis: ( r <= 0 & s < 0 implies r + s < 0 )
assume r <= 0 ; :: thesis: ( not s < 0 or r + s < 0 )
then r + s <= 0 + s by Lm5;
hence ( not s < 0 or r + s < 0 ) by Lm6; :: thesis: verum