for X1, X2 being set
for S1 being non empty Subset-Family of X1
for S2 being non empty Subset-Family of X2 holds { s where s is Subset of [:X1,X2:] : ex x1, x2 being set st
( x1 in S1 & x2 in S2 & s = [:x1,x2:] ) } = { [:x1,x2:] where x1 is Element of S1, x2 is Element of S2 : verum }