let X be finite set ; :: thesis: for C being Subset-Family of X st C is (C1) & C is (C2) 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 (C2) implies 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 } ;
A1: [#] X = X ;
{ 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 object ; :: 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 Th33;
assume A2: C is (C1) ; :: thesis: ( not C is (C2) or ex F being Full-family of X st C = candidate-keys F )
assume A3: C is (C2) ; :: thesis: ex F being Full-family of X st C = candidate-keys F
A4: now :: thesis: for x being set st x in C holds
[x,X] in Maximal_wrt F
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 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
A6: c in BB and
A7: 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 A6;
hence X c= c by A5, A7; :: thesis: verum
end;
then [x9,X] in F by A1;
then consider a, b being Subset of X such that
A8: [a,b] in Maximal_wrt F and
A9: [a,b] >= [x9,([#] X)] by Th26;
A10: a c= x9 by A9;
X c= b by A9;
then A11: b = X by XBOOLE_0:def 10;
assume A12: not [x,X] in Maximal_wrt F ; :: 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 A13: K in C ; :: thesis: not K c= a
assume A14: K c= a ; :: thesis: contradiction
then K c= x9 by A10;
then K = x9 by A3, A5, A13;
hence contradiction by A8, A10, A11, A12, A14, XBOOLE_0:def 10; :: thesis: verum
end;
then a in BB ;
then X c= a by A8, A11, Lm3;
then X = a by XBOOLE_0:def 10;
hence contradiction by A8, A10, A11, A12, XBOOLE_0:def 10; :: thesis: verum
end;
take F ; :: thesis: C = candidate-keys F
now :: thesis: for x being object holds
( ( x in C implies x in candidate-keys F ) & ( x in candidate-keys F implies x in C ) )
let x be object ; :: 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 A15: 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 A15; :: thesis: verum
end;
assume x in candidate-keys F ; :: thesis: x in C
then consider A being Subset of X such that
A16: x = A and
A17: [A,X] in Maximal_wrt F ;
assume A18: not x in C ; :: thesis: contradiction
now :: thesis: for K being Subset of X holds
( not K in C or not K c= A )
A19: A ^|^ X,F by A17;
given K being Subset of X such that A20: K in C and
A21: K c= A ; :: thesis: contradiction
A22: [K,([#] X)] >= [A,([#] X)] by A21;
[K,X] in Maximal_wrt F by A4, A20;
hence contradiction by A16, A18, A20, A19, A22, Th27; :: thesis: verum
end;
then A23: A in BB ;
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
A24: c in BB and
A25: not c = X ; :: thesis: not A c= c
assume A c= c ; :: thesis: contradiction
then X c= c by A1, A17, A24, Lm3;
hence contradiction by A24, A25, XBOOLE_0:def 10; :: thesis: verum
end;
then X in BB by A23;
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 ) ) ;
then for K being object holds not K in C ;
hence contradiction by A2, XBOOLE_0:def 1; :: thesis: verum
end;
hence C = candidate-keys F by TARSKI:2; :: thesis: verum