:: deftheorem Def7 defines discerning METRIC_1:def 7 :
for M being MetrStruct holds
( M is discerning iff the distance of M is discerning );