:: deftheorem Def1 defines bounded_metric METRIC_6:def 1 :
for A being non empty set
for G, b₃ being Function of [:A,A:],REAL holds
( b₃ = bounded_metric (A,G) iff for a, b being Element of A holds b₃ . (a,b) = (G . (a,b)) / (1 + (G . (a,b))) );