:: deftheorem defines is_generator-set_of ARMSTRNG:def 25 :
for X, G being set
for B being Subset-Family of X holds
( G is_generator-set_of B iff ( G c= B & B = { (Intersect S) where S is Subset-Family of X : S c= G } ) );