for n being non zero Nat holds Infty_dist n is_metric_of REAL n