:: deftheorem defines is_dst METRIC_2:def 5 :
for M being non empty MetrStruct
for V, Q being Element of M -neighbour
for v being Real holds
( V,Q is_dst v iff for p, q being Element of M st p in V & q in Q holds
dist (p,q) = v );