let X be set ; :: thesis: for S being cap-finite-partition-closed diff-finite-partition-closed Subset-Family of X holds { (union x) where x is finite Subset of S : x is mutually-disjoint } is cup-closed
let S be cap-finite-partition-closed diff-finite-partition-closed Subset-Family of X; :: thesis: { (union x) where x is finite Subset of S : x is mutually-disjoint } is cup-closed
set Y = { (union x) where x is finite Subset of S : x is mutually-disjoint } ;
let a, b be set ; :: according to FINSUB_1:def 1 :: thesis: ( not a in { (union x) where x is finite Subset of S : x is mutually-disjoint } or not b in { (union x) where x is finite Subset of S : x is mutually-disjoint } or a \/ b in { (union x) where x is finite Subset of S : x is mutually-disjoint } )
assume A: ( a in { (union x) where x is finite Subset of S : x is mutually-disjoint } & b in { (union x) where x is finite Subset of S : x is mutually-disjoint } ) ; :: thesis: a \/ b in { (union x) where x is finite Subset of S : x is mutually-disjoint }
then consider a0 being finite Subset of S such that
B: ( a = union a0 & a0 is mutually-disjoint ) ;
consider b0 being finite Subset of S such that
C: ( b = union b0 & b0 is mutually-disjoint ) by A;
consider SM being FinSequence such that
F1: rng SM = a0 \/ b0 by FINSEQ_1:52;
consider P being finite Subset of S such that
VU: P is a_partition of Union SM and
for Y being Element of rng SM holds Y = union { s where s is Element of S : ( s in P & s c= Y ) } by F1, Thm87;
Union SM = (union a0) \/ (union b0) by F1, ZFMISC_1:78;
then VB: union P = a \/ b by B, C, VU, EQREL_1:def 4;
for x, y being set st x in P & y in P & x <> y holds
x misses y by VU, EQREL_1:def 4;
then P is mutually-disjoint by TAXONOM2:def 5;
hence a \/ b in { (union x) where x is finite Subset of S : x is mutually-disjoint } by VB; :: thesis: verum