let X be set ; :: thesis: for S being cap-finite-partition-closed Subset-Family of X holds { (union x) where x is finite Subset of S : x is mutually-disjoint } is cap-closed
let S be cap-finite-partition-closed Subset-Family of X; :: thesis: { (union x) where x is finite Subset of S : x is mutually-disjoint } is cap-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 2 :: 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 that
H3: a in { (union x) where x is finite Subset of S : x is mutually-disjoint } and
H4: 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 }
a /\ b in { (union x) where x is finite Subset of S : x is mutually-disjoint }
proof
consider xa being finite Subset of S such that
V1: a = union xa and
V2: xa is mutually-disjoint by H3;
consider xb being finite Subset of S such that
V3: b = union xb and
V4: xb is mutually-disjoint by H4;
consider p being finite Subset of S such that
K2: p is a_partition of (union xa) /\ (union xb) by V2, V4, V;
K3: union p = a /\ b by V1, V3, K2, EQREL_1:def 4;
for x, y being set st x in p & y in p & x <> y holds
x misses y by K2, 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 K3; :: thesis: verum
end;
hence a /\ b in { (union x) where x is finite Subset of S : x is mutually-disjoint } ; :: thesis: verum