theorem Th5: :: SPPOL_1:5

for n being Nat
for u1, u2 being Point of (Euclid n)
for v1, v2 being Element of REAL n st v1 = u1 & v2 = u2 holds
dist (u1,u2) = |.(v1 - v2).|