for X, Y being set
for A being Subset of X
for B being Subset of Y holds <:(pr2 (X,Y)),(pr1 (X,Y)):> .: [:A,B:] = [:B,A:]