:: deftheorem Def7 defines Infty_dist SRINGS_5:def 20 :
for n being non zero Nat
for b₂ being Function of [:(REAL n),(REAL n):],REAL holds
( b₂ = Infty_dist n iff for x, y being Element of REAL n holds b₂ . (x,y) = sup (rng (abs (x - y))) );