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