theorem Th35: :: ARMSTRNG:35

for X being non empty finite set
for B being Subset-Family of X st B is (B1) & B is (B2) holds
( B = saturated-subsets (X deps_encl_by B) & ( for G being Full-family of X st B = saturated-subsets G holds
G = X deps_encl_by B ) )