let X be finite set ; :: thesis: for F being Dependency-set of X
for K being Subset of X st F = { [A,B] where A, B is Subset of X : ( K c= A or B c= A ) } holds
candidate-keys F = {K}
let F be Dependency-set of X; :: thesis: for K being Subset of X st F = { [A,B] where A, B is Subset of X : ( K c= A or B c= A ) } holds
candidate-keys F = {K}
let K be Subset of X; :: thesis: ( F = { [A,B] where A, B is Subset of X : ( K c= A or B c= A ) } implies candidate-keys F = {K} )
assume A1: F = { [A,B] where A, B is Subset of X : ( K c= A or B c= A ) } ; :: thesis: candidate-keys F = {K}
A2: Maximal_wrt F = {[K,X]} \/ { [A,A] where A is Subset of X : not K c= A } by A1, Th32;

now

let x be set ; :: thesis: ( ( x in candidate-keys F implies x in {K} ) & ( x in {K} implies x in candidate-keys F ) )

hereby :: thesis: ( x in {K} implies x in candidate-keys F )

assume x in candidate-keys F ; :: thesis: x in {K}
then consider a being Subset of X such that
A3: x = a and
A4: [a,X] in Maximal_wrt F ;

per cases ( [a,X] in {[K,X]} or [a,X] in { [A,A] where A is Subset of X : not K c= A } ) by A2, A4, XBOOLE_0:def 3;

suppose [a,X] in {[K,X]} ; :: thesis: x in {K}

then [a,X] = [K,X] by TARSKI:def 1;
then a = K by ZFMISC_1:33;
hence x in {K} by A3, TARSKI:def 1; :: thesis: verum

end;

suppose [a,X] in { [A,A] where A is Subset of X : not K c= A } ; :: thesis: x in {K}

then consider A being Subset of X such that
A5: [a,X] = [A,A] and
A6: not K c= A ;
( a = A & X = A ) by A5, ZFMISC_1:33;
hence x in {K} by A6; :: thesis: verum

end;

end;

end;

assume x in {K} ; :: thesis: x in candidate-keys F
then A7: x = K by TARSKI:def 1;
[K,X] in {[K,X]} by TARSKI:def 1;
then [K,X] in Maximal_wrt F by A2, XBOOLE_0:def 3;
hence x in candidate-keys F by A7; :: thesis: verum

end;

hence candidate-keys F = {K} by TARSKI:2; :: thesis: verum