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