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