:: deftheorem Def6 defines Pitag_dist EUCLID:def 6 :
for n being Nat
for b₂ being Function of [:(REAL n),(REAL n):],REAL holds
( b₂ = Pitag_dist n iff for x, y being Element of REAL n holds b₂ . (x,y) = |.(x - y).| );