theorem :: FUNCT_4:145

for a, c, b, d, x, y, z, w being object st a,c,x,w are_mutually_distinct holds
(a,c,x,w) --> (b,d,y,z) = {[a,b],[c,d],[x,y],[w,z]}