let X be finite set ; :: thesis:
let C be Subset-Family of X; :: thesis:
let B be set ; :: thesis:
assume that
A1: C is (C1) and
A2: C is without_proper_subsets and
A3: B = { b where b is Subset of X : for K being Subset of X st K in C holds
not K c= b } ; :: thesis:
set F = X deps_encl_by B;
B c= bool X

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in B ; :: thesis:
then ex b being Subset of X st
( x = b & ( for K being Subset of X st K in C holds
not K c= b ) ) by A3;
hence x in bool X ; :: thesis:

end;

then reconsider BB = B as Subset-Family of X ;
A4: [#] X = X ;

A5: now

let x be set ; :: thesis:
assume A6: x in C ; :: thesis:
then reconsider x' = x as Subset of X ;

let c be set ; :: thesis:
assume A7: ( c in BB & x' c= c ) ; :: thesis:
then ex b being Subset of X st
( c = b & ( for K being Subset of X st K in C holds
not K c= b ) ) by A3;
hence X c= c by A6, A7; :: thesis:

end;

then [x',X] in X deps_encl_by B by A4;
then consider a, b being Subset of X such that
A8: [a,b] in Maximal_wrt (X deps_encl_by B) and
A9: [a,b] >= [x',([#] X)] by Th28;
A10: a c= x' by A9, Th15;
X c= b by A9, Th15;
then A11: b = X by XBOOLE_0:def 10;
assume A12: not [x,X] in Maximal_wrt (X deps_encl_by B) ; :: thesis:

let K be Subset of X; :: thesis:
assume A13: K in C ; :: thesis:
assume A14: K c= a ; :: thesis:
then K c= x' by A10, XBOOLE_1:1;
then K = x' by A2, A6, A13, Def28;
hence contradiction by A8, A10, A11, A12, A14, XBOOLE_0:def 10; :: thesis:

end;

then a in BB by A3;
then X c= a by A8, A11, Lm2;
then X = a by XBOOLE_0:def 10;
hence contradiction by A8, A10, A11, A12, XBOOLE_0:def 10; :: thesis:

end;

now

let x be set ; :: thesis:

hereby :: thesis:

assume A15: x in C ; :: thesis:
then [x,X] in Maximal_wrt (X deps_encl_by B) by A5;
hence x in candidate-keys (X deps_encl_by B) by A15; :: thesis:

end;

assume x in candidate-keys (X deps_encl_by B) ; :: thesis:
then consider A being Subset of X such that
A16: x = A and
A17: [A,X] in Maximal_wrt (X deps_encl_by B) ;
A18: for c being set holds
( not c in BB or c = X or not A c= c )

let c be set ; :: thesis:
assume that
A19: c in BB and
A20: not c = X ; :: thesis:
consider cb being Subset of X such that
A21: c = cb and
for K being Subset of X st K in C holds
not K c= cb by A3, A19;
assume A c= c ; :: thesis:
then X c= c by A4, A17, A19, Lm2;
hence contradiction by A20, A21, XBOOLE_0:def 10; :: thesis:

end;

assume A22: not x in C ; :: thesis:

given K being Subset of X such that A23: K in C and
A24: K c= A ; :: thesis:
A25: [K,X] in Maximal_wrt (X deps_encl_by B) by A5, A23;
A26: A ^|^ X,X deps_encl_by B by A17, Def18;
[K,([#] X)] >= [A,([#] X)] by A24, Th15;
hence contradiction by A16, A22, A23, A25, A26, Th29; :: thesis:

end;

then A in BB by A3;
then X in BB by A18;
then consider b being Subset of X such that
A27: b = X and
A28: for K being Subset of X st K in C holds
not K c= b by A3;
for K being set holds not K in C by A27, A28;
hence contradiction by A1, XBOOLE_0:def 1; :: thesis:

end;

hence C = candidate-keys (X deps_encl_by B) by TARSKI:2; :: thesis: