let X be finite set ; :: thesis: for C being Subset-Family of X
for B being set st C is (C1) & C is (C2) & B = { b where b is Subset of X : for K being Subset of X st K in C holds
not K c= b } holds
C = candidate-keys (X deps_encl_by B)
let C be Subset-Family of X; :: thesis: for B being set st C is (C1) & C is (C2) & B = { b where b is Subset of X : for K being Subset of X st K in C holds
not K c= b } holds
C = candidate-keys (X deps_encl_by B)
let B be set ; :: thesis: ( C is (C1) & C is (C2) & B = { b where b is Subset of X : for K being Subset of X st K in C holds
not K c= b } implies C = candidate-keys (X deps_encl_by B) )
assume that
A1: C is (C1) and
A2: C is (C2) 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: C = candidate-keys (X deps_encl_by B)
B c= bool X

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in bool X )
assume x in B ; :: thesis: x in bool X
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: verum

end;

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

A5: now :: thesis: for x being set st x in C holds
[x,X] in Maximal_wrt (X deps_encl_by B)

let x be set ; :: thesis: ( x in C implies [x,X] in Maximal_wrt (X deps_encl_by B) )
assume A6: x in C ; :: thesis: [x,X] in Maximal_wrt (X deps_encl_by B)
then reconsider x9 = x as Subset of X ;

now :: thesis: for c being set st c in BB & x9 c= c holds
X c= c

let c be set ; :: thesis: ( c in BB & x9 c= c implies X c= c )
assume that
A7: c in BB and
A8: x9 c= c ; :: thesis: X c= c
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, A7;
hence X c= c by A6, A8; :: thesis: verum

end;

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

now :: thesis: for K being Subset of X st K in C holds
not K c= a

let K be Subset of X; :: thesis: ( K in C implies not K c= a )
assume A14: K in C ; :: thesis: not K c= a
assume A15: K c= a ; :: thesis: contradiction
then K c= x9 by A11;
then K = x9 by A2, A6, A14;
hence contradiction by A9, A11, A12, A13, A15, XBOOLE_0:def 10; :: thesis: verum

end;

then a in BB by A3;
then X c= a by A9, A12, Lm3;
then X = a by XBOOLE_0:def 10;
hence contradiction by A9, A11, A12, A13, XBOOLE_0:def 10; :: thesis: verum

end;

now :: thesis: for x being object holds
( ( x in C implies x in candidate-keys (X deps_encl_by B) ) & ( x in candidate-keys (X deps_encl_by B) implies x in C ) )

let x be object ; :: thesis: ( ( x in C implies x in candidate-keys (X deps_encl_by B) ) & ( x in candidate-keys (X deps_encl_by B) implies x in C ) )

hereby :: thesis: ( x in candidate-keys (X deps_encl_by B) implies x in C )

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

end;

assume x in candidate-keys (X deps_encl_by B) ; :: thesis: x in C
then consider A being Subset of X such that
A17: x = A and
A18: [A,X] in Maximal_wrt (X deps_encl_by B) ;
assume A19: not x in C ; :: thesis: contradiction

now :: thesis: for K being Subset of X holds
( not K in C or not K c= A )

A20: A ^|^ X,X deps_encl_by B by A18;
given K being Subset of X such that A21: K in C and
A22: K c= A ; :: thesis: contradiction
A23: [K,([#] X)] >= [A,([#] X)] by A22;
[K,X] in Maximal_wrt (X deps_encl_by B) by A5, A21;
hence contradiction by A17, A19, A21, A20, A23, Th27; :: thesis: verum

end;

then A24: A in BB by A3;
for c being set holds
( not c in BB or c = X or not A c= c )

proof

let c be set ; :: thesis: ( not c in BB or c = X or not A c= c )
assume that
A25: c in BB and
A26: not c = X ; :: thesis: not A c= c
assume A c= c ; :: thesis: contradiction
then X c= c by A4, A18, A25, Lm3;
hence contradiction by A25, A26, XBOOLE_0:def 10; :: thesis: verum

end;

then X in BB by A24;
then ex b being Subset of X st
( b = X & ( for K being Subset of X st K in C holds
not K c= b ) ) by A3;
then for K being object holds not K in C ;
hence contradiction by A1, XBOOLE_0:def 1; :: thesis: verum

end;

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