for M being PseudoMetricSpace
for V, Q being Element of M -neighbour
for v being Real holds
( V,Q is_dst v iff ex p, q being Element of M st
( p in V & q in Q & dist (p,q) = v ) )