:: deftheorem defines -neighbour METRIC_2:def 4 :
for M being non empty MetrStruct holds M -neighbour = { s where s is Subset of M : ex x being Element of M st x -neighbour = s } ;