let X be set ; :: thesis: ( X is cap-closed & X is cup-closed implies X is Ring_of_sets )
assume ( X is cap-closed & X is cup-closed ) ; :: thesis: X is Ring_of_sets
then for x, y being set st x in X & y in X holds
( x /\ y in X & x \/ y in X ) ;
hence X is Ring_of_sets by COHSP_1:def 7, LATTICE7:def 8; :: thesis: verum