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