for A being non empty set
for G being Function of [:A,A:],REAL st G is_metric_of A holds
bounded_metric (A,G) is_metric_of A