let a, b, c, d be real number ; :: thesis: ( a + b <= c + d iff a - c <= d - b )
thus ( a + b <= c + d implies a - c <= d - b ) by Lm20; :: thesis: ( a - c <= d - b implies a + b <= c + d )
assume A1: a - c <= d - b ; :: thesis: a + b <= c + d
assume c + d < a + b ; :: thesis: contradiction
then d < (b + a) - c by Lm19;
then d < b + (a - c) ;
hence contradiction by A1, Lm17; :: thesis: verum