let X be set ; :: thesis: for D being a_partition of X holds UniCl D is Ring_of_sets
let D be a_partition of X; :: thesis: UniCl D is Ring_of_sets
set DU = { (union P) where P is Subset of D : verum } ;
( UniCl D is V288() & UniCl D is cup-closed ) ;
then ( { (union P) where P is Subset of D : verum } is cap-closed & { (union P) where P is Subset of D : verum } is cup-closed ) by Th14;
then for x, y being set st x in { (union P) where P is Subset of D : verum } & y in { (union P) where P is Subset of D : verum } holds
( x /\ y in { (union P) where P is Subset of D : verum } & x \/ y in { (union P) where P is Subset of D : verum } ) ;
then { (union P) where P is Subset of D : verum } is Ring_of_sets by COHSP_1:def 7, LATTICE7:def 8;
hence UniCl D is Ring_of_sets by Th14; :: thesis: verum