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 7 :: thesis: ( not a in A or not b in A or ( a /\ b in A & a \/ b in A ) )
assume that
A1: a in A and
A2: b in A ; :: thesis: ( a /\ b in A & a \/ b in A )
a = {} by A1, TARSKI:def 1;
hence ( a /\ b in A & a \/ b in A ) by A2, TARSKI:def 1; :: thesis: verum
end;
hence ( A is Ring_of_sets & not A is empty ) by Def8; :: thesis: verum