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