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