theorem THY2: :: GTARSKI2:10

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