let X1, X2 be set ; :: thesis: for S1 being Subset-Family of X1
for S2 being Subset-Family of X2 holds { s where s is Subset of [:X1,X2:] : ex s1, s2 being set st
( s1 in S1 & s2 in S2 & s = [:s1,s2:] ) } is Subset-Family of [:X1,X2:]
let S1 be Subset-Family of X1; :: thesis: for S2 being Subset-Family of X2 holds { s where s is Subset of [:X1,X2:] : ex s1, s2 being set st
( s1 in S1 & s2 in S2 & s = [:s1,s2:] ) } is Subset-Family of [:X1,X2:]
let S2 be Subset-Family of X2; :: thesis: { s where s is Subset of [:X1,X2:] : ex s1, s2 being set st
( s1 in S1 & s2 in S2 & s = [:s1,s2:] ) } is Subset-Family of [:X1,X2:]
set S = { s where s is Subset of [:X1,X2:] : ex s1, s2 being set st
( s1 in S1 & s2 in S2 & s = [:s1,s2:] ) } ;
{ s where s is Subset of [:X1,X2:] : ex s1, s2 being set st
( s1 in S1 & s2 in S2 & s = [:s1,s2:] ) } c= bool [:X1,X2:]

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { s where s is Subset of [:X1,X2:] : ex s1, s2 being set st
( s1 in S1 & s2 in S2 & s = [:s1,s2:] ) } or x in bool [:X1,X2:] )
assume x in { s where s is Subset of [:X1,X2:] : ex s1, s2 being set st
( s1 in S1 & s2 in S2 & s = [:s1,s2:] ) } ; :: thesis: x in bool [:X1,X2:]
then consider s0 being Subset of [:X1,X2:] such that
A1: ( x = s0 & ex s1, s2 being set st
( s1 in S1 & s2 in S2 & s0 = [:s1,s2:] ) ) ;
thus x in bool [:X1,X2:] by A1; :: thesis: verum

end;

hence { s where s is Subset of [:X1,X2:] : ex s1, s2 being set st
( s1 in S1 & s2 in S2 & s = [:s1,s2:] ) } is Subset-Family of [:X1,X2:] ; :: thesis: verum