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