:: deftheorem defines ev_eq_1 METRIC_2:def 6 :
for M being non empty MetrStruct
for V, Q being Element of M -neighbour holds ev_eq_1 (V,Q) = { v where v is Element of REAL : V,Q is_dst v } ;