let a, b be Real; :: thesis: ( a < - b implies a + b < 0 )
assume a < - b ; :: thesis: a + b < 0
then a + b < (- b) + b by Lm10;
hence a + b < 0 ; :: thesis: verum