theorem Th63: :: SRINGS_5:96

(Pitag_dist 2) . (|[0,0]|,|[1,1]|) = sqrt 2