let X be non empty finite set ; :: thesis:
let F be Dependency-set of X; :: thesis:
let K be Subset of X; :: thesis:
set dcF = Dependency-closure F;
set S = { P where P is Subset of X : [K,P] in Dependency-closure F } ;
{ P where P is Subset of X : [K,P] in Dependency-closure F } c= bool X

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { P where P is Subset of X : [K,P] in Dependency-closure F } ; :: thesis:
then ex P being Subset of X st
( x = P & [K,P] in Dependency-closure F ) ;
hence x in bool X ; :: thesis:

end;

then reconsider S = { P where P is Subset of X : [K,P] in Dependency-closure F } as Subset-Family of X ;
set ck = candidate-keys (Dependency-closure F);
set B = { c where c is Subset of X : for x, y being Subset of X st [x,y] in F & x c= c holds
y c= c } ;
[K,K] in Dependency-closure F by Def11;
then K in S ;
then consider m being set such that
A1: m in S and
A2: for B being set st B in S & m c= B holds
B = m by FINSET_1:6;
{ c where c is Subset of X : for x, y being Subset of X st [x,y] in F & x c= c holds
y c= c } = enclosure_of F ;
then A3: Dependency-closure F = X deps_encl_by { c where c is Subset of X : for x, y being Subset of X st [x,y] in F & x c= c holds
y c= c } by Th38;

hereby :: thesis:

assume K in candidate-keys (Dependency-closure F) ; :: thesis:
then consider A being Subset of X such that
A4: K = A and
A5: [A,X] in Maximal_wrt (Dependency-closure F) ;
A6: A ^|^ X, Dependency-closure F by A5;
[A,([#] X)] in Dependency-closure F by A5;
then consider a, b being Subset of X such that
A7: [A,X] = [a,b] and
A8: for c being set st c in { c where c is Subset of X : for x, y being Subset of X st [x,y] in F & x c= c holds
y c= c } & a c= c holds
b c= c by A3;
A9: X = b by A7, XTUPLE_0:1;
A10: A = a by A7, XTUPLE_0:1;
thus K is_p_i_w_ncv_of F :: thesis:

hereby :: according to ARMSTRNG:def 32 :: thesis:

let z be Subset of X; :: thesis:
assume that
A11: K c= z and
A12: z <> X and
A13: not z in charact_set F ; :: thesis:
for x, y being Subset of X st [x,y] in F & x c= z holds
y c= z by A13;
then z in { c where c is Subset of X : for x, y being Subset of X st [x,y] in F & x c= c holds
y c= c } ;
then X c= z by A4, A8, A10, A9, A11;
hence contradiction by A12, XBOOLE_0:def 10; :: thesis:

end;

let k be set ; :: thesis:
assume A14: k c< K ; :: thesis:
then k c= A by A4, XBOOLE_0:def 8;
then reconsider k = k as Subset of X by XBOOLE_1:1;
set S = { P where P is Subset of X : [k,P] in Dependency-closure F } ;
{ P where P is Subset of X : [k,P] in Dependency-closure F } c= bool X

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in { P where P is Subset of X : [k,P] in Dependency-closure F } ; :: thesis:
then ex P being Subset of X st
( x = P & [k,P] in Dependency-closure F ) ;
hence x in bool X ; :: thesis:

end;

then reconsider S = { P where P is Subset of X : [k,P] in Dependency-closure F } as Subset-Family of X ;
[k,k] in Dependency-closure F by Def11;
then k in S ;
then consider m being set such that
A15: m in S and
A16: for B being set st B in S & m c= B holds
B = m by FINSET_1:6;
consider P being Subset of X such that
A17: m = P and
A18: [k,P] in Dependency-closure F by A15;
[k,k] in Dependency-closure F by Def11;
then A19: [(k \/ k),(k \/ P)] in Dependency-closure F by A18, Def13;
assume A20: for a being Subset of X holds
( not k c= a or not a <> X or a in charact_set F ) ; :: thesis:
A21: [k,([#] X)] in Dependency-closure F

suppose k \/ P = X ; :: thesis:

hence [k,([#] X)] in Dependency-closure F by A19; :: thesis:

end;

suppose k \/ P <> X ; :: thesis:

then k \/ P in charact_set F by A20, XBOOLE_1:7;
then k \/ P in charact_set (Dependency-closure F) by Th59;
then consider x, y being Subset of X such that
A22: [x,y] in Dependency-closure F and
A23: x c= k \/ P and
A24: not y c= k \/ P by Th55;
[(k \/ P),(k \/ P)] in Dependency-closure F by Def11;
then [(x \/ (k \/ P)),(y \/ (k \/ P))] in Dependency-closure F by A22, Def13;
then [(k \/ P),(y \/ (k \/ P))] in Dependency-closure F by A23, XBOOLE_1:12;
then [k,(y \/ (k \/ P))] in Dependency-closure F by A19, Th18;
then A25: y \/ (k \/ P) in S ;
P c= k \/ P by XBOOLE_1:7;
then P = y \/ (k \/ P) by A16, A17, A25, XBOOLE_1:10;
hence [k,([#] X)] in Dependency-closure F by A24, XBOOLE_1:7, XBOOLE_1:10; :: thesis:

end;

end;

end;

k c= K by A14, XBOOLE_0:def 8;
then [K,([#] X)] <= [k,([#] X)] ;
hence contradiction by A4, A6, A14, A21, Th27; :: thesis:

end;

end;

consider P being Subset of X such that
A26: m = P and
A27: [K,P] in Dependency-closure F by A1;
[K,K] in Dependency-closure F by Def11;
then A28: [(K \/ K),(K \/ P)] in Dependency-closure F by A27, Def13;
assume A29: K is_p_i_w_ncv_of F ; :: thesis:
A30: K c= K \/ P by XBOOLE_1:7;
A31: [K,([#] X)] in Dependency-closure F

suppose K \/ P = X ; :: thesis:

hence [K,([#] X)] in Dependency-closure F by A28; :: thesis:

end;

suppose K \/ P <> X ; :: thesis:

then K \/ P in charact_set F by A29, A30;
then K \/ P in charact_set (Dependency-closure F) by Th59;
then consider x, y being Subset of X such that
A32: [x,y] in Dependency-closure F and
A33: x c= K \/ P and
A34: not y c= K \/ P by Th55;
[(K \/ P),(K \/ P)] in Dependency-closure F by Def11;
then [(x \/ (K \/ P)),(y \/ (K \/ P))] in Dependency-closure F by A32, Def13;
then [(K \/ P),(y \/ (K \/ P))] in Dependency-closure F by A33, XBOOLE_1:12;
then [K,(y \/ (K \/ P))] in Dependency-closure F by A28, Th18;
then A35: y \/ (K \/ P) in S ;
P c= K \/ P by XBOOLE_1:7;
then P = y \/ (K \/ P) by A2, A26, A35, XBOOLE_1:10;
hence [K,([#] X)] in Dependency-closure F by A34, XBOOLE_1:7, XBOOLE_1:10; :: thesis:

end;

end;

end;

let x9, y9 be Subset of X; :: thesis:
assume that
A36: [x9,y9] in Dependency-closure F and
A37: ( K <> x9 or X <> y9 ) and
A38: [K,([#] X)] <= [x9,y9] ; :: thesis:
A39: X c= y9 by A38;
x9 c= K by A38;
then x9 c< K by A37, A39, XBOOLE_0:def 8, XBOOLE_0:def 10;
then consider a being Subset of X such that
A40: x9 c= a and
A41: a <> X and
A42: not a in charact_set F by A29;
X = y9 by A39, XBOOLE_0:def 10;
then A43: not y9 c= a by A41, XBOOLE_0:def 10;
not a in charact_set (Dependency-closure F) by A42, Th59;
hence contradiction by A36, A40, A43; :: thesis:

end;

then K ^|^ X, Dependency-closure F by A31, Th27;
then [K,X] in Maximal_wrt (Dependency-closure F) ;
hence K in candidate-keys (Dependency-closure F) ; :: thesis: