theorem :: SRINGS_5:106

Pitag_dist 2 <> Infty_dist 2