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