theorem :: MEASUR10:8

for X, Y being set
for M being with_empty_element Subset-Family of X
for N being with_empty_element Subset-Family of Y holds { [:A,B:] where A is Element of M, B is Element of N : verum } is with_empty_element Subset-Family of [:X,Y:]