:: deftheorem Def10 defines well_dist COMPL_SP:def 10 :
for M being MetrStruct
for a being Point of M
for X being set
for b₄ being Function of [:([:X,( the carrier of M \ {a}):] \/ {[X,a]}),([:X,( the carrier of M \ {a}):] \/ {[X,a]}):],REAL holds
( b₄ = well_dist (a,X) iff for x, y being Element of [:X,( the carrier of M \ {a}):] \/ {[X,a]}
for x1, y1 being object
for x2, y2 being Point of M st x = [x1,x2] & y = [y1,y2] holds
( ( x1 = y1 implies b₄ . (x,y) = dist (x2,y2) ) & ( x1 <> y1 implies b₄ . (x,y) = (dist (x2,a)) + (dist (a,y2)) ) ) );