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