:: deftheorem Def3 defines equivalence_class METRIC_2:def 3 :
for M being non empty MetrStruct
for b₂ being Subset of M holds
( b₂ is equivalence_class of M iff ex x being Element of M st b₂ = x -neighbour );