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, Lm8;
hence b < a + c ; :: thesis: verum