let a, b, c be Real; :: thesis: ( a <= b iff c - b <= c - a )

hereby :: thesis: ( c - b <= c - a implies a <= b )

assume a <= b ; :: thesis: c - b <= c - a
then - b <= - a by Lm14;
then c + (- b) <= c + (- a) by Lm5;
hence c - b <= c - a ; :: thesis: verum

end;

assume c - b <= c - a ; :: thesis: a <= b
then (c - b) - c <= (c - a) - c by Th9;
then - b <= - a ;
hence a <= b by Lm15; :: thesis: verum