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