let X be finite set ; :: thesis: for C being Subset-Family of X st C is (C1) & C is without_proper_subsets holds
ex F being Full-family of X st C = candidate-keys F
let C be Subset-Family of X; :: thesis: ( C is (C1) & C is without_proper_subsets implies ex F being Full-family of X st C = candidate-keys F )
assume A1: C is (C1) ; :: thesis: ( not C is without_proper_subsets or ex F being Full-family of X st C = candidate-keys F )
assume A2: C is without_proper_subsets ; :: thesis: ex F being Full-family of X st C = candidate-keys F
set B = { b where b is Subset of X : for K being Subset of X st K in C holds
not K c= b } ;
{ b where b is Subset of X : for K being Subset of X st K in C holds
not K c= b } c= bool X

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { b where b is Subset of X : for K being Subset of X st K in C holds
not K c= b } or x in bool X )
assume x in { b where b is Subset of X : for K being Subset of X st K in C holds
not K c= 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 ) ) ;
hence x in bool X ; :: thesis: verum

end;

then reconsider BB = { b where b is Subset of X : for K being Subset of X st K in C holds
not K c= b } as Subset-Family of X ;
set F = { [a,b] where a, b is Subset of X : for c being set st c in BB & a c= c holds
b c= c } ;
{ [a,b] where a, b is Subset of X : for c being set st c in BB & a c= c holds
b c= c } = X deps_encl_by BB ;
then reconsider F = { [a,b] where a, b is Subset of X : for c being set st c in BB & a c= c holds
b c= c } as Full-family of X by Th35;
take F ; :: thesis: C = candidate-keys F
A3: [#] X = X ;

A4: now

let x be set ; :: thesis: ( x in C implies [x,X] in Maximal_wrt F )
assume A5: x in C ; :: thesis: [x,X] in Maximal_wrt F
then reconsider x' = x as Subset of X ;

now

let c be set ; :: thesis: ( c in BB & x' c= c implies X c= c )
assume A6: ( c in BB & x' c= c ) ; :: thesis: X c= c
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 ) ) ;
hence X c= c by A5, A6; :: thesis: verum

end;

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

now

let K be Subset of X; :: thesis: ( K in C implies not K c= a )
assume A12: K in C ; :: thesis: not K c= a
assume A13: K c= a ; :: thesis: contradiction
then K c= x' by A9, XBOOLE_1:1;
then K = x' by A2, A5, A12, Def28;
hence contradiction by A7, A9, A10, A11, A13, XBOOLE_0:def 10; :: thesis: verum

end;

then a in BB ;
then X c= a by A7, A10, Lm2;
then X = a by XBOOLE_0:def 10;
hence contradiction by A7, A9, A10, A11, XBOOLE_0:def 10; :: thesis: verum

end;

now

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

hereby :: thesis: ( x in candidate-keys F implies x in C )

assume A14: x in C ; :: thesis: x in candidate-keys F
then [x,X] in Maximal_wrt F by A4;
hence x in candidate-keys F by A14; :: thesis: verum

end;

assume x in candidate-keys F ; :: thesis: x in C
then consider A being Subset of X such that
A15: x = A and
A16: [A,X] in Maximal_wrt F ;
A17: 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
A18: c in BB and
A19: not c = X ; :: thesis: not A c= c
consider cb being Subset of X such that
A20: c = cb and
for K being Subset of X st K in C holds
not K c= cb by A18;
assume A c= c ; :: thesis: contradiction
then X c= c by A3, A16, A18, Lm2;
hence contradiction by A19, A20, XBOOLE_0:def 10; :: thesis: verum

end;

assume A21: not x in C ; :: thesis: contradiction

now

given K being Subset of X such that A22: K in C and
A23: K c= A ; :: thesis: contradiction
A24: [K,X] in Maximal_wrt F by A4, A22;
A25: A ^|^ X,F by A16, Def18;
[K,([#] X)] >= [A,([#] X)] by A23, Th15;
hence contradiction by A15, A21, A22, A24, A25, Th29; :: thesis: verum

end;

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

end;

hence C = candidate-keys F by TARSKI:2; :: thesis: verum