let X1, X2 be set ; 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; 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; { 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 ;
TARSKI:def 3 ( 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:] ) }
;
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;
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:]
; verum