theorem Th2: :: METRIC_1:2

for M being MetrStruct holds
( ( for a, b being Element of M st dist (a,b) = 0 holds
a = b ) iff M is discerning )