for a, b, x, y, X, Y being set st a <> b & x in X & y in Y holds
(a,b) --> (x,y) in product ((a,b) --> (X,Y))