let a, b be Real; :: 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