:: deftheorem Def10 defines discrete_dist METRIC_1:def 10 :
for A being set
for b₂ being Function of [:A,A:],REAL holds
( b₂ = discrete_dist A iff for x, y being Element of A holds
( b₂ . (x,x) = 0 & ( x <> y implies b₂ . (x,y) = 1 ) ) );