let c, a, b be real number ; :: thesis: ( c <= a & c <= b & a -' c = b -' c implies a = b )
assume A1: ( a >= c & b >= c & a -' c = b -' c ) ; :: thesis: a = b
then a - c >= 0 by Th50;
then A2: a -' c = a - c by XREAL_0:def 2;
b - c >= 0 by A1, Th50;
then a + (- c) = b + (- c) by A1, A2, XREAL_0:def 2;
hence a = b ; :: thesis: verum