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 a + b < c by Th39;
hence b < c - a by Lm19; :: thesis: verum