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