theorem :: SRINGS_5:100

Pitag_dist 1 = Infty_dist 1