theorem Th7: :: TOPREAL3:7

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