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