:: deftheorem Def1 defines Eucl_dist JORDAN_A:def 1 :
for n being Nat
for b₂ being RealMap of [:(TOP-REAL n),(TOP-REAL n):] holds
( b₂ = Eucl_dist n iff for p, q being Point of (TOP-REAL n) holds b₂ . (p,q) = |.(p - q).| );