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 Lm10;
hence contradiction by A1; :: thesis: verum