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:]

( s1 in S1 & s2 in S2 & s = [:s1,s2:] ) } is Subset-Family of [:X1,X2:] ; :: thesis: verum

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

hence
{ s where s is Subset of [:X1,X2:] : ex s1, s2 being set st
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;( 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

( s1 in S1 & s2 in S2 & s = [:s1,s2:] ) } is Subset-Family of [:X1,X2:] ; :: thesis: verum