theorem :: ARMSTRNG:48

for R being DB-Rel holds
( candidate-keys (Dependency-str R) is (C1) & candidate-keys (Dependency-str R) is (C2) )