let X1, X2 be set ; :: thesis: for F1 being Field_Subset of X1
for F2 being Field_Subset of X2 holds { [:A,B:] where A is Element of F1, B is Element of F2 : verum } is semialgebra_of_sets of [:X1,X2:]
let F1 be Field_Subset of X1; :: thesis: for F2 being Field_Subset of X2 holds { [:A,B:] where A is Element of F1, B is Element of F2 : verum } is semialgebra_of_sets of [:X1,X2:]
let F2 be Field_Subset of X2; :: thesis: { [:A,B:] where A is Element of F1, B is Element of F2 : verum } is semialgebra_of_sets of [:X1,X2:]
set S = { [:A,B:] where A is Element of F1, B is Element of F2 : verum } ;
( F1 is semialgebra_of_sets of X1 & F2 is semialgebra_of_sets of X2 ) by SRINGS_3:20;
hence { [:A,B:] where A is Element of F1, B is Element of F2 : verum } is semialgebra_of_sets of [:X1,X2:] by Th09; :: thesis: verum