let n be Element of NAT ; :: thesis: for x, y, z being Point of (TOP-REAL n) st x + y = x + z holds
y = z
let x, y, z be Point of (TOP-REAL n); :: thesis: ( x + y = x + z implies y = z )
assume x + y = x + z ; :: thesis: y = z
then (x - x) + y = (x + z) - x by JORDAN2C:7;
then ( x - x = 0. (TOP-REAL n) & (x - x) + y = (x - x) + z ) by EUCLID:42, JORDAN2C:7;
hence y = (0. (TOP-REAL n)) + z by EUCLID:27
.= z by EUCLID:27 ;
:: thesis: verum