for x, y, X being set holds Swap ((id X),x,y) is one-to-one