:: deftheorem Def8 defines Ring_of_sets LATTICE7:def 8 :
for b₁ being set holds
( b₁ is Ring_of_sets iff b₁ includes_lattice_of b₁ );