let a, b, c be Real; :: 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, Th36;
hence b < c - a by Lm19; :: thesis: verum