for X, Y being set holds <:(pr2 (X,Y)),(pr1 (X,Y)):> is one-to-one