:: deftheorem defines charact_set ARMSTRNG:def 31 :
for X being set
for F being Dependency-set of X holds charact_set F = { A where A is Subset of X : ex a, b being Subset of X st
( [a,b] in F & a c= A & not b c= A ) } ;