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