theorem Th62: :: SRINGS_5:95

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