( S1 is semialgebra_of_sets of X1 & S2 is semialgebra_of_sets of X2 ) by SRINGS_3:20;
hence { [:A,B:] where A is Element of S1, B is Element of S2 : verum } is semialgebra_of_sets of [:X1,X2:] by Th09; :: thesis: verum