for N being Nat
for p1, p2 being Point of (TOP-REAL N)
for x1, x2 being Point of (Euclid N) st x1 = p1 & x2 = p2 holds
|.(p1 - p2).| = dist (x1,x2)