let a, b, c be Real; :: thesis: ( 0 < a & b <= c implies b < a + c )
assume ( 0 < a & b <= c ) ; :: thesis: b < a + c
then b + 0 < a + c by Lm8;
hence b < a + c ; :: thesis: verum