:: deftheorem defines candidate-keys ARMSTRNG:def 26 :
for X being set
for F being Dependency-set of X holds candidate-keys F = { A where A is Subset of X : [A,X] in Maximal_wrt F } ;