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