for p1, p2 being Point of (TOP-REAL 3)
for u1, u2 being Point of (Euclid 3) st u1 = p1 & u2 = p2 holds
(Pitag_dist 3) . (u1,u2) = sqrt (((((p1 `1) - (p2 `1)) ^2) + (((p1 `2) - (p2 `2)) ^2)) + (((p1 `3) - (p2 `3)) ^2))