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 Lm5;
hence a + b <= 0 ; :: thesis: verum