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