theorem :: ARMSTRNG:49

for X being finite set
for C being Subset-Family of X st C is (C1) & C is (C2) holds
ex F being Full-family of X st C = candidate-keys F