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