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 F = { [A,B] where A, B is Subset of X : ( K c= A or B c= A ) } ; :: thesis: candidate-keys F = {K}
then A1: Maximal_wrt F = {[K,X]} \/ { [A,A] where A is Subset of X : not K c= A } by Th30;

now :: thesis: for x being object holds
( ( x in candidate-keys F implies x in {K} ) & ( x in {K} implies x in candidate-keys F ) )

let x be object ; :: 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
A2: x = a and
A3: [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 A1, A3, 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 XTUPLE_0:1;
hence x in {K} by A2, 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
A4: [a,X] = [A,A] and
A5: not K c= A ;
X = A by A4, XTUPLE_0:1;
hence x in {K} by A5; :: thesis: verum

end;

end;

end;

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

end;

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