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 Ring_of_sets
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 Ring_of_sets
( { (union x) where x is finite Subset of S : x is mutually-disjoint } is cap-closed & { (union x) where x is finite Subset of S : x is mutually-disjoint } is cup-closed ) by Thm86, thmCup;
hence { (union x) where x is finite Subset of S : x is mutually-disjoint } is Ring_of_sets by thmIL; :: thesis: verum