:: deftheorem defines ev_eq_2 METRIC_2:def 7 :
for M being non empty MetrStruct
for v being Element of REAL holds ev_eq_2 (v,M) = { W where W is Element of [:(M -neighbour),(M -neighbour):] : ex V, Q being Element of M -neighbour st
( W = [V,Q] & V,Q is_dst v ) } ;