let a, b, c be Real; :: thesis: ( a - b <= c implies a - c <= b )
assume c >= a - b ; :: thesis: a - c <= b
then c + b >= a by Lm19;
hence a - c <= b by Lm18; :: thesis: verum