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