theorem :: ARMSTRNG:42

for X being non empty finite set
for G being Subset-Family of X holds G is_generator-set_of saturated-subsets (X deps_encl_by G)