let X be set ; :: thesis: for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X holds DisUnion S is cap-closed
let S be with_empty_element cap-closed semi-diff-closed Subset-Family of X; :: thesis: DisUnion S is cap-closed
set P = DisUnion S;
now :: thesis: for x, y being set st x in DisUnion S & y in DisUnion S holds
x /\ y in DisUnion S
let x, y be set ; :: thesis: ( x in DisUnion S & y in DisUnion S implies x /\ y in DisUnion S )
assume C1: ( x in DisUnion S & y in DisUnion S ) ; :: thesis: x /\ y in DisUnion S
then consider x1 being Subset of X such that
C2: ( x = x1 & ex g being disjoint_valued FinSequence of S st x1 = Union g ) ;
consider g1 being disjoint_valued FinSequence of S such that
C3: x1 = Union g1 by C2;
consider y1 being Subset of X such that
C4: ( y = y1 & ex g being disjoint_valued FinSequence of S st y1 = Union g ) by C1;
consider g2 being disjoint_valued FinSequence of S such that
C5: y1 = Union g2 by C4;
consider h being disjoint_valued FinSequence such that
C6: ( (Union g1) /\ (Union g2) = Union h & dom h = Seg ((len g1) * (len g2)) & ( for i being Nat st i in dom h holds
h . i = (g1 . (((i -' 1) div (len g2)) + 1)) /\ (g2 . (((i -' 1) mod (len g2)) + 1)) ) ) by TT2;
x1 /\ y1 c= X ;
then reconsider xy = x /\ y as Subset of X by C2, C4;
now :: thesis: for i being Nat st i in dom h holds
h . i in S
let i be Nat; :: thesis: ( i in dom h implies h . i in S )
assume C9: i in dom h ; :: thesis: h . i in S
then ( ((i -' 1) mod (len g2)) + 1 in dom g2 & ((i -' 1) div (len g2)) + 1 in dom g1 ) by C6, Lem10;
then ( g1 . (((i -' 1) div (len g2)) + 1) in S & g2 . (((i -' 1) mod (len g2)) + 1) in S ) by FINSEQ_2:11;
then (g1 . (((i -' 1) div (len g2)) + 1)) /\ (g2 . (((i -' 1) mod (len g2)) + 1)) in S by FINSUB_1:def 2;
hence h . i in S by C9, C6; :: thesis: verum
end;
then reconsider h = h as disjoint_valued FinSequence of S by FINSEQ_2:12;
xy = Union h by C2, C4, C3, C5, C6;
hence x /\ y in DisUnion S ; :: thesis: verum
end;
hence DisUnion S is cap-closed ; :: thesis: verum