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