let a, b, c be Real; :: 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