let a, b, c, d be Real; :: thesis: ( a <= b & c <= d implies a - d <= b - c )
assume A1: a <= b ; :: thesis: ( not c <= d or a - d <= b - c )
assume c <= d ; :: thesis: a - d <= b - c
then - d <= - c by Lm14;
then a + (- d) <= b + (- c) by A1, Lm6;
hence a - d <= b - c ; :: thesis: verum