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