let a, b, c be real number ; :: thesis: ( 0 < a & b <= c implies b - a < c )
assume that
A1: 0 < a and
A2: b <= c ; :: thesis: b - a < c
b + 0 < a + c by A1, A2, Th41;
hence b - a < c by Lm17; :: thesis: verum