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