theorem Th57: :: ARMSTRNG:57

for X being non empty finite set
for F being Dependency-set of X holds
( ( for A, B being Subset of X holds
( [A,B] in Dependency-closure F iff for a being Subset of X st A c= a & not B c= a holds
a in charact_set F ) ) & saturated-subsets (Dependency-closure F) = (bool X) \ (charact_set F) )