let X1, X2 be set ; for S1 being semialgebra_of_sets of X1
for S2 being semialgebra_of_sets of X2 holds { [:A,B:] where A is Element of S1, B is Element of S2 : verum } is semialgebra_of_sets of [:X1,X2:]
let S1 be semialgebra_of_sets of X1; for S2 being semialgebra_of_sets of X2 holds { [:A,B:] where A is Element of S1, B is Element of S2 : verum } is semialgebra_of_sets of [:X1,X2:]
let S2 be semialgebra_of_sets of X2; { [:A,B:] where A is Element of S1, B is Element of S2 : verum } is semialgebra_of_sets of [:X1,X2:]
set S = { [:A,B:] where A is Element of S1, B is Element of S2 : verum } ;
A1:
{ [:A,B:] where A is Element of S1, B is Element of S2 : verum } is Semiring of [:X1,X2:]
by Th08;
( X1 in S1 & X2 in S2 )
by SRINGS_3:def 6;
then
[:X1,X2:] in { [:A,B:] where A is Element of S1, B is Element of S2 : verum }
;
hence
{ [:A,B:] where A is Element of S1, B is Element of S2 : verum } is semialgebra_of_sets of [:X1,X2:]
by A1, SRINGS_3:def 6; verum