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 - (b - d) <= - (a - c) by Tk1, Lm14;
hence d - b <= c - a ; :: thesis: verum