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