let X1, X2 be set ; :: thesis: for S1 being Subset-Family of X1
for S2 being Subset-Family of X2 st S1 is cap-closed & S2 is cap-closed holds
{ 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
let S1 be Subset-Family of X1; :: thesis: for S2 being Subset-Family of X2 st S1 is cap-closed & S2 is cap-closed holds
{ 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
let S2 be Subset-Family of X2; :: thesis: ( S1 is cap-closed & S2 is cap-closed implies { 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 )
assume A1: S1 is cap-closed ; :: thesis: ( not S2 is cap-closed or { 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 )
assume A2: S2 is cap-closed ; :: thesis: { 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
set Y = { 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 cap-closed

proof

let W1, W2 be set ; :: according to FINSUB_1:def 2 :: thesis: ( not W1 in { s where s is Subset of [:X1,X2:] : ex x1, x2 being set st
( x1 in S1 & x2 in S2 & s = [:x1,x2:] ) } or not W2 in { s where s is Subset of [:X1,X2:] : ex x1, x2 being set st
( x1 in S1 & x2 in S2 & s = [:x1,x2:] ) } or W1 /\ W2 in { s where s is Subset of [:X1,X2:] : ex x1, x2 being set st
( x1 in S1 & x2 in S2 & s = [:x1,x2:] ) } )
assume A3: W1 in { s where s is Subset of [:X1,X2:] : ex x1, x2 being set st
( x1 in S1 & x2 in S2 & s = [:x1,x2:] ) } ; :: thesis: ( not W2 in { s where s is Subset of [:X1,X2:] : ex x1, x2 being set st
( x1 in S1 & x2 in S2 & s = [:x1,x2:] ) } or W1 /\ W2 in { s where s is Subset of [:X1,X2:] : ex x1, x2 being set st
( x1 in S1 & x2 in S2 & s = [:x1,x2:] ) } )
assume A4: W2 in { s where s is Subset of [:X1,X2:] : ex x1, x2 being set st
( x1 in S1 & x2 in S2 & s = [:x1,x2:] ) } ; :: thesis: W1 /\ W2 in { s where s is Subset of [:X1,X2:] : ex x1, x2 being set st
( x1 in S1 & x2 in S2 & s = [:x1,x2:] ) }
consider s1 being Subset of [:X1,X2:] such that
A5: ( W1 = s1 & ex xs1, xs2 being set st
( xs1 in S1 & xs2 in S2 & s1 = [:xs1,xs2:] ) ) by A3;
consider xs1, xs2 being set such that
A6: ( xs1 in S1 & xs2 in S2 & s1 = [:xs1,xs2:] ) by A5;
consider s2 being Subset of [:X1,X2:] such that
A7: ( W2 = s2 & ex ys1, ys2 being set st
( ys1 in S1 & ys2 in S2 & s2 = [:ys1,ys2:] ) ) by A4;
consider ys1, ys2 being set such that
A8: ( ys1 in S1 & ys2 in S2 & s2 = [:ys1,ys2:] ) by A7;
A9: [:xs1,xs2:] /\ [:ys1,ys2:] = [:(xs1 /\ ys1),(xs2 /\ ys2):] by ZFMISC_1:100;
A10: ( xs1 /\ ys1 in S1 & xs2 /\ ys2 in S2 ) by A6, A8, A1, A2, FINSUB_1:def 2;
s1 /\ s2 in { s where s is Subset of [:X1,X2:] : ex x1, x2 being set st
( x1 in S1 & x2 in S2 & s = [:x1,x2:] ) } by A6, A8, A9, A10;
hence W1 /\ W2 in { s where s is Subset of [:X1,X2:] : ex x1, x2 being set st
( x1 in S1 & x2 in S2 & s = [:x1,x2:] ) } by A5, A7; :: thesis: verum

end;

hence { 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 ; :: thesis: verum