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