theorem :: SRINGS_5:101

Pitag_dist 2 <> Infty_dist 2