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