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