take A = {{} }; :: thesis: ( A is Ring_of_sets & not A is empty )
A includes_lattice_of A

proof

let a, b be set ; :: according to COHSP_1:def 8 :: thesis: ( not a in A or not b in A or ( a /\ b in A & a \/ b in A ) )
assume ( a in A & b in A ) ; :: thesis: ( a /\ b in A & a \/ b in A )
then ( a = {} & b = {} ) by TARSKI:def 1;
hence ( a /\ b in A & a \/ b in A ) by TARSKI:def 1; :: thesis: verum

end;

hence ( A is Ring_of_sets & not A is empty ) by Def8; :: thesis: verum