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