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:31
.= p + (p1 - p1) by EUCLID:46
.= (p + p1) - p1 by EUCLID:49
.= q + (p1 - p1) by A1, EUCLID:49
.= q + (0. (TOP-REAL n)) by EUCLID:46
.= q by EUCLID:31 ; :: thesis: verum