:: deftheorem defines Eq_classMetricSpace METRIC_2:def 14 :
for M being PseudoMetricSpace holds Eq_classMetricSpace M = MetrStruct(# (M -neighbour),(nbourdist M) #);