theorem Th05: :: MEASUR10:7

for X1, X2 being set
for S1 being non empty Subset-Family of X1
for S2 being non empty Subset-Family of X2 holds { [:a,b:] where a is Element of S1, b is Element of S2 : verum } is non empty Subset-Family of [:X1,X2:]