theorem THY3: :: GTARSKI2:11

dist (|[1,0]|,|[0,1]|) = sqrt 2