:: deftheorem defines discerning METRIC_1:def 3 :
for A being set
for f being PartFunc of [:A,A:],REAL holds
( f is discerning iff for a, b being Element of A st f . (a,b) = 0 holds
a = b );