let a, b, c, d be real number ; :: thesis: ( a < b & c <= d implies a - d < b - c )
assume that
A1: a < b and
A2: c <= d ; :: thesis: a - d < b - c
- d <= - c by A2, Lm14;
then a + (- d) < b + (- c) by A1, Lm8;
hence a - d < b - c ; :: thesis: verum