:: deftheorem defines Discerning METRIC_1:def 17 :
for A being non empty set
for f being Function of [:A,A:],REAL holds
( f is Discerning iff for a, b being Element of A st a <> b holds
0 < f . (a,b) );