theorem :: YELLOW_9:42

for X1, X2 being set
for A being Subset-Family of [:X1,X2:]
for A1 being non empty Subset-Family of X1
for A2 being non empty Subset-Family of X2 st A = { [:a,b:] where a is Subset of X1, b is Subset of X2 : ( a in A1 & b in A2 ) } holds
Intersect A = [:(Intersect A1),(Intersect A2):]