theorem :: ARMSTRNG:51

for X being non empty finite set
for C being Subset-Family of X st C is (C1) & C is (C2) holds
ex R being DB-Rel st
( the Attributes of R = X & C = candidate-keys (Dependency-str R) )