let D be DB-Rel ; :: thesis: ( candidate-keys (Dependency-str D) is (C1) & candidate-keys (Dependency-str D) is (C2) )
set F = Dependency-str D;
set X = the Attributes of D;
A1: Dependency-str D is full_family by Th23;
then A2: Maximal_wrt (Dependency-str D) is (M2) by Th28;
saturated-subsets (Dependency-str D) is (B1) by A1, Th32;
then the Attributes of D in saturated-subsets (Dependency-str D) ;
then consider B, A being Subset of the Attributes of D such that
A3: the Attributes of D = B and
A4: A ^|^ B, Dependency-str D by Th31;
[A, the Attributes of D] in Maximal_wrt (Dependency-str D) by A3, A4;
then A in candidate-keys (Dependency-str D) ;
hence not candidate-keys (Dependency-str D) is empty ; :: thesis: candidate-keys (Dependency-str D) is (C2)
let k1, k2 be set ; :: according to ARMSTRNG:def 27 :: thesis: ( k1 in candidate-keys (Dependency-str D) & k2 in candidate-keys (Dependency-str D) & k1 c= k2 implies k1 = k2 )
assume that
A5: k1 in candidate-keys (Dependency-str D) and
A6: k2 in candidate-keys (Dependency-str D) and
A7: k1 c= k2 ; :: thesis: k1 = k2
consider a2 being Subset of the Attributes of D such that
A8: k2 = a2 and
A9: [a2, the Attributes of D] in Maximal_wrt (Dependency-str D) by A6;
consider a1 being Subset of the Attributes of D such that
A10: k1 = a1 and
A11: [a1, the Attributes of D] in Maximal_wrt (Dependency-str D) by A5;
[a1,([#] the Attributes of D)] >= [a2,([#] the Attributes of D)] by A7, A10, A8;
hence k1 = k2 by A10, A11, A8, A9, A2; :: thesis: verum