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

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

assume A1: a <= b ; :: thesis: not c - a < c - b
assume c - a < c - b ; :: thesis: contradiction
then - (c - b) < - (c - a) by Lm15;
then b - c < a - c ;
hence contradiction by A1, Lm7; :: thesis: verum

end;

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