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 Lm15;
then a + (- d) < b + (- c) by A1, Lm8;
hence a - d < b - c ; :: thesis: verum