theorem :: METRIC_2:16

for M being non empty MetrStruct
for x being Element of M holds x -neighbour in M -neighbour ;