let n be Element of NAT ; :: thesis: for p, p1, q being Point of (TOP-REAL n) st p + p1 = q + p1 holds
p = q
let p, p1, q be Point of (TOP-REAL n); :: thesis: ( p + p1 = q + p1 implies p = q )
assume A1: p + p1 = q + p1 ; :: thesis: p = q
thus p = p + (0. (TOP-REAL n)) by EUCLID:27
.= p + (p1 - p1) by EUCLID:42
.= (p + p1) - p1 by EUCLID:45
.= q + (p1 - p1) by A1, EUCLID:45
.= q + (0. (TOP-REAL n)) by EUCLID:42
.= q by EUCLID:27 ; :: thesis: verum