let a be Real; :: thesis: ( - 1 < a implies 0 < 1 + a )
assume - 1 < a ; :: thesis: 0 < 1 + a
then (- 1) + 1 < a + 1 by Lm8;
hence 0 < 1 + a ; :: thesis: verum