theorem Th65: :: SRINGS_5:98

for x, y being Element of REAL 1 holds (Infty_dist 1) . (x,y) = |.((x . 1) - (y . 1)).|