theorem Th64: :: SRINGS_5:97

(Infty_dist 2) . (|[0,0]|,|[1,1]|) = 1