theorem ThEquiv: :: GTARSKI2:12

for n being Nat
for p, q being POINT of (TarskiEuclidSpace n)
for p1, q1 being Element of (TOP-REAL n) st p = p1 & q = q1 holds
( dist (p,q) = (Pitag_dist n) . (p1,q1) & dist (p,q) = |.(p1 - q1).| )