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