theorem ThConv: :: GTARSKI2:15

for n being Nat
for p, q being Element of (TarskiEuclidSpace n)
for p1, q1 being Element of (Euclid n) st p = p1 & q = q1 holds
dist (p,q) = dist (p1,q1)