for X being finite set
for C being Subset-Family of X
for B being set st C is (C1) & C is (C2) & B = { b where b is Subset of X : for K being Subset of X st K in C holds
not K c= b } holds
C = candidate-keys (X deps_encl_by B)