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