let M be non empty MetrSpace; :: thesis: M is Discerning
for a, b being Element of M st a <> b holds
0 < dist (a,b) by Lm8;
hence M is Discerning by Th26; :: thesis: verum