theorem Th7: :: METRIC_2:7

for M being PseudoMetricSpace
for x, y being Element of M st y in x -neighbour holds
x -neighbour = y -neighbour