let a, b, c be Real; :: thesis: ( a <= b implies a - c <= b - c )
( a <= b implies a + (- c) <= b + (- c) ) by Lm5;
hence ( a <= b implies a - c <= b - c ) ; :: thesis: verum