for n being Nat
for p, p1, q being Point of (TOP-REAL n) st p1 + p = p1 + q holds
p = q by Th3;