theorem Th17: :: METRIC_2:17

for V being set
for M being non empty MetrStruct holds
( V in M -neighbour iff V is equivalence_class of M )