:: deftheorem Def22 defines Eukl_dist3 METRIC_3:def 22 :
for b₁ being Function of [:[:REAL,REAL,REAL:],[:REAL,REAL,REAL:]:],REAL holds
( b₁ = Eukl_dist3 iff for x1, y1, x2, y2, x3, y3 being Element of REAL
for x, y being Element of [:REAL,REAL,REAL:] st x = [x1,x2,x3] & y = [y1,y2,y3] holds
b₁ . (x,y) = sqrt ((((real_dist . (x1,y1)) ^2) + ((real_dist . (x2,y2)) ^2)) + ((real_dist . (x3,y3)) ^2)) );