let a, b be Real; :: thesis: ( a <= - b implies b <= - a )
assume a <= - b ; :: thesis: b <= - a
then - (- b) <= - a by Lm14;
hence b <= - a ; :: thesis: verum