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 Th7;
hence M is Discerning by Th25; :: thesis: verum