:: deftheorem defines elem_in_rel_2 METRIC_2:def 10 :
for M being non empty MetrStruct holds elem_in_rel_2 M = { Q where Q is Element of M -neighbour : ex V being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v } ;