let D be DB-Rel ; :: thesis: ( candidate-keys (Dependency-str D) is (C1) & candidate-keys (Dependency-str D) is without_proper_subsets )
set F = Dependency-str D;
set X = the Attributes of D;
A1: Dependency-str D is full_family by Th25;
then saturated-subsets (Dependency-str D) is (B1) by Th34;
then the Attributes of D in saturated-subsets (Dependency-str D) by Def4;
then consider B, A being Subset of the Attributes of D such that
A2: ( the Attributes of D = B & A ^|^ B, Dependency-str D ) by Th33;
[A,the Attributes of D] in Maximal_wrt (Dependency-str D) by A2, Def18;
then A in candidate-keys (Dependency-str D) ;
hence candidate-keys (Dependency-str D) is (C1) ; :: thesis: candidate-keys (Dependency-str D) is without_proper_subsets
let k1, k2 be set ; :: according to ARMSTRNG:def 28 :: thesis: ( k1 in candidate-keys (Dependency-str D) & k2 in candidate-keys (Dependency-str D) & k1 c= k2 implies k1 = k2 )
assume that
A3: k1 in candidate-keys (Dependency-str D) and
A4: k2 in candidate-keys (Dependency-str D) and
A5: k1 c= k2 ; :: thesis: k1 = k2
consider a1 being Subset of the Attributes of D such that
A6: k1 = a1 and
A7: [a1,the Attributes of D] in Maximal_wrt (Dependency-str D) by A3;
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 A4;
A10: Maximal_wrt (Dependency-str D) is (M2) by A1, Th30;
[a1,([#] the Attributes of D)] >= [a2,([#] the Attributes of D)] by A5, A6, A8, Th15;
hence k1 = k2 by A6, A7, A8, A9, A10, Def20; :: thesis: verum