for M being non empty MetrStruct holds
( ( for a, b being Element of M st a <> b holds
0 < dist (a,b) ) iff M is Discerning )