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 )
A1: x - x = 0. (TOP-REAL n) by EUCLID:46;
assume x + y = x + z ; :: thesis: y = z
then (x - x) + y = (x + z) - x by JORDAN2C:9;
then (x - x) + y = (x - x) + z by JORDAN2C:9;
hence y = (0. (TOP-REAL n)) + z by A1, EUCLID:31
.= z by EUCLID:31 ;
:: thesis: verum