let a, b, c be Real; :: 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, Lm6;
hence b <= a + c ; :: thesis: verum