theorem THY1: :: GTARSKI2:9

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