let a, b, c, d be Real; :: 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 a - c <= d - b ; :: thesis: a + b <= c + d
then (a - c) + b <= (d - b) + b by Lm5;
then ((a - c) + b) + c <= d + c by Lm5;
hence a + b <= c + d ; :: thesis: verum