let b, a be real number ; :: thesis: ( - b <= a implies - a <= b )
assume A1: - b <= a ; :: thesis: - a <= b
assume b < - a ; :: thesis: contradiction
then b + a < (- a) + a by Lm10;
then a - (- b) < 0 ;
hence contradiction by A1, Lm22; :: thesis: verum