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