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