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