:: deftheorem defines -neighbour METRIC_2:def 2 :
for M being non empty MetrStruct
for x being Element of M holds x -neighbour = { y where y is Element of M : x tolerates y } ;