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