for n being non zero Nat
for x, y being Element of REAL n ex S being ext-real-membered set st
( S = { |.((x . i) - (y . i)).| where i is Element of Seg n : verum } & (Infty_dist n) . (x,y) = sup S )