:: deftheorem defines Field_generated_by SRINGS_3:def 7 :
for X being set
for S being semialgebra_of_sets of X holds Field_generated_by S = meet { Z where Z is Field_Subset of X : S c= Z } ;