:: deftheorem defines GeneratorSet FREEALG:def 4 :
for U0 being Universal_Algebra
for b₂ being Subset of U0 holds
( b₂ is GeneratorSet of U0 iff for A being Subset of U0 st A is opers_closed & b₂ c= A holds
A = the carrier of U0 );