theorem :: SRINGS_5:105

Pitag_dist 1 = Infty_dist 1