let X1, X2 be set ; :: thesis: for S1 being cap-closed semiring_of_sets of X1
for S2 being cap-closed semiring_of_sets of X2 holds { [:s1,s2:] where s1 is Element of S1, s2 is Element of S2 : verum } is cap-closed semiring_of_sets of [:X1,X2:]
let S1 be cap-closed semiring_of_sets of X1; :: thesis: for S2 being cap-closed semiring_of_sets of X2 holds { [:s1,s2:] where s1 is Element of S1, s2 is Element of S2 : verum } is cap-closed semiring_of_sets of [:X1,X2:]
let S2 be cap-closed semiring_of_sets of X2; :: thesis: { [:s1,s2:] where s1 is Element of S1, s2 is Element of S2 : verum } is cap-closed semiring_of_sets of [:X1,X2:]
set S = { s where s is Subset of [:X1,X2:] : ex x1, x2 being set st
( x1 in S1 & x2 in S2 & s = [:x1,x2:] ) } ;
( { s where s is Subset of [:X1,X2:] : ex x1, x2 being set st
( x1 in S1 & x2 in S2 & s = [:x1,x2:] ) } is semiring_of_sets of [:X1,X2:] & { s where s is Subset of [:X1,X2:] : ex x1, x2 being set st
( x1 in S1 & x2 in S2 & s = [:x1,x2:] ) } is cap-closed ) by SRINGS_2:7, SRINGS_2:3;
hence { [: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_2:2; :: thesis: verum