let a, b, c be Real; ( c <= a & c <= b & a -' c = b -' c implies a = b )
assume that
A1:
a >= c
and
A2:
b >= c
and
A3:
a -' c = b -' c
; a = b
a - c >= 0
by A1, Th48;
then A4:
a -' c = a - c
by XREAL_0:def 2;
b - c >= 0
by A2, Th48;
then
a + (- c) = b + (- c)
by A3, A4, XREAL_0:def 2;
hence
a = b
; verum