:: deftheorem defines enclosure_of ARMSTRNG:def 23 :
for X being set
for F being Dependency-set of X holds enclosure_of F = { b where b is Subset of X : for A, B being Subset of X st [A,B] in F & A c= b holds
B c= b } ;