let X1, X2 be set ; :: thesis: for S1 being semialgebra_of_sets of X1
for S2 being semialgebra_of_sets of X2 holds { [:s1,s2:] where s1 is Element of S1, s2 is Element of S2 : verum } is semialgebra_of_sets of [:X1,X2:]
let S1 be semialgebra_of_sets of X1; :: thesis: for S2 being semialgebra_of_sets of X2 holds { [:s1,s2:] where s1 is Element of S1, s2 is Element of S2 : verum } is semialgebra_of_sets of [:X1,X2:]
let S2 be semialgebra_of_sets of X2; :: thesis: { [:s1,s2:] where s1 is Element of S1, s2 is Element of S2 : verum } is semialgebra_of_sets of [:X1,X2:]
set S = { [:s1,s2:] where s1 is Element of S1, s2 is Element of S2 : verum } ;
( S1 is cap-closed semiring_of_sets of X1 & S2 is cap-closed semiring_of_sets of X2 ) by SRINGS_3:9;
then { [:s1,s2:] where s1 is Element of S1, s2 is Element of S2 : verum } is cap-closed semiring_of_sets of [:X1,X2:] by SRINGS_4:36;
then A1: { [:s1,s2:] where s1 is Element of S1, s2 is Element of S2 : verum } is with_empty_element cap-closed semi-diff-closed Subset-Family of [:X1,X2:] by SRINGS_3:10;
( X1 in S1 & X2 in S2 ) by SRINGS_3:def 6;
then [:X1,X2:] in { [:s1,s2:] where s1 is Element of S1, s2 is Element of S2 : verum } ;
hence { [:s1,s2:] where s1 is Element of S1, s2 is Element of S2 : verum } is semialgebra_of_sets of [:X1,X2:] by A1, SRINGS_3:def 6; :: thesis: verum