:: deftheorem Def13 defines nbourdist METRIC_2:def 13 :
for M being PseudoMetricSpace
for b₂ being Function of [:(M -neighbour),(M -neighbour):],REAL holds
( b₂ = nbourdist M iff for V, Q being Element of M -neighbour
for p, q being Element of M st p in V & q in Q holds
b₂ . (V,Q) = dist (p,q) );