:: deftheorem defines Ring_generated_by SRINGS_3:def 2 :
for X being set
for S being with_empty_element cap-closed semi-diff-closed Subset-Family of X holds Ring_generated_by S = meet { Z where Z is non empty preBoolean Subset-Family of X : S c= Z } ;