theorem Th3: :: GOBOARD7:3

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