let X be finite set ; 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; ( 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
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)
; ( not C is (C2) or ex F being Full-family of X st C = candidate-keys F )
assume A3:
C is (C2)
; ex F being Full-family of X st C = candidate-keys F
A4:
now for x being set st x in C holds
[x,X] in Maximal_wrt Flet x be
set ;
( x in C implies [x,X] in Maximal_wrt F )assume A5:
x in C
;
[x,X] in Maximal_wrt Fthen reconsider x9 =
x as
Subset of
X ;
now for c being set st c in BB & x9 c= c holds
X c= clet c be
set ;
( c in BB & x9 c= c implies X c= c )assume that A6:
c in BB
and A7:
x9 c= c
;
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;
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
;
contradictionthen
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;
verum end;
take
F
; C = candidate-keys F
now 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 ;
( ( x in C implies x in candidate-keys F ) & ( x in candidate-keys F implies x in C ) )assume
x in candidate-keys F
;
x in Cthen 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
;
contradictionnow 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
;
contradictionA22:
[K,([#] X)] >= [A,([#] X)]
by A21;
[K,X] in Maximal_wrt F
by A4, A20;
hence
contradiction
by A16, A18, A20, A19, A22, Th27;
verum end; then A23:
A in BB
;
for
c being
set holds
( not
c in BB or
c = X or not
A c= c )
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;
verum end;
hence
C = candidate-keys F
by TARSKI:2; verum