theorem Th31: :: ARMSTRNG:31

for X, x being set
for F being Dependency-set of X holds
( x in saturated-subsets F iff ex B, A being Subset of X st
( x = B & A ^|^ B,F ) )