:: deftheorem defines saturated-subsets ARMSTRNG:def 21 :
for X being set
for F being Dependency-set of X holds saturated-subsets F = { B where B is Subset of X : ex A being Subset of X st A ^|^ B,F } ;