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