:: deftheorem defines Discerning METRIC_1:def 18 :
for M being non empty MetrStruct holds
( M is Discerning iff the distance of M is Discerning );