let X be non empty finite set ; :: thesis:
let C be Subset-Family of X; :: thesis:
assume that
A1: C is (C1) and
A2: C is without_proper_subsets ; :: thesis:
set M = { L where L is Subset of X : for K being Subset of X st K in C holds
L /\ K <> {} } ;
0 in {0 } by TARSKI:def 1;
then A3: 0 in { L where L is Subset of X : for K being Subset of X st K in C holds
L /\ K <> {} } \/ {0 } by XBOOLE_0:def 3;
reconsider M0 = { L where L is Subset of X : for K being Subset of X st K in C holds
L /\ K <> {} } \/ {0 } as non empty set ;
reconsider D = X --> (bool X) as non-empty ManySortedSet of ;
set R = { ((X --> 0 ) +* (L --> L)) where L is Subset of X : L in M0 } ;
A4: (X --> 0 ) +* (({} X) --> ({} X)) in { ((X --> 0 ) +* (L --> L)) where L is Subset of X : L in M0 } by A3;
{ ((X --> 0 ) +* (L --> L)) where L is Subset of X : L in M0 } c= product D

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume x in { ((X --> 0 ) +* (L --> L)) where L is Subset of X : L in M0 } ; :: thesis:
then consider L being Subset of X such that
A5: x = (X --> 0 ) +* (L --> L) and
L in M0 ;
set g = (X --> 0 ) +* (L --> L);
A6: dom (L --> L) = L by FUNCOP_1:19;
then A7: dom ((X --> 0 ) +* (L --> L)) = (dom (X --> 0 )) \/ L by FUNCT_4:def 1
.= X \/ L by FUNCOP_1:19
.= X by XBOOLE_1:12 ;
A8: dom D = X by PARTFUN1:def 4;

now

let x be set ; :: thesis:
assume A9: x in dom D ; :: thesis:
A10: D . x = bool X by A8, A9, FUNCOP_1:13;

per cases ;

suppose A11: x in L ; :: thesis:

then ((X --> 0 ) +* (L --> L)) . x = (L --> L) . x by A6, FUNCT_4:14
.= L by A11, FUNCOP_1:13 ;
hence ((X --> 0 ) +* (L --> L)) . x in D . x by A10; :: thesis:

end;

suppose not x in L ; :: thesis:

then ((X --> 0 ) +* (L --> L)) . x = (X --> 0 ) . x by A6, FUNCT_4:12
.= {} X by A8, A9, FUNCOP_1:13 ;
hence ((X --> 0 ) +* (L --> L)) . x in D . x by A10; :: thesis:

end;

hence x in product D by A5, A7, A8, CARD_3:def 5; :: thesis:

end;

then reconsider R = { ((X --> 0 ) +* (L --> L)) where L is Subset of X : L in M0 } as non empty Subset of (product D) by A4;
take DB = DB-Rel(# X,D,R #); :: thesis:
thus the Attributes of DB = X ; :: thesis:
set ds = Dependency-str DB;
set ck = { A where A is Subset of X : [A,X] in Maximal_wrt (Dependency-str DB) } ;
A12: [#] X = X ;

A13: now

let x be set ; :: thesis:
assume A14: x in C ; :: thesis:
then reconsider A = x as Subset of X ;
reconsider AA = A, XA = X as Subset of the Attributes of DB by A12;

now

let f, g be Element of the Relationship of DB; :: thesis:
assume A15: f | A = g | A ; :: thesis:
f in R ;
then consider Lf being Subset of X such that
A16: f = (X --> 0 ) +* (Lf --> Lf) and
A17: Lf in M0 ;
g in R ;
then consider Lg being Subset of X such that
A18: g = (X --> 0 ) +* (Lg --> Lg) and
A19: Lg in M0 ;
A20: ( ( Lf in { L where L is Subset of X : for K being Subset of X st K in C holds
L /\ K <> {} } or Lf in {0 } ) & ( Lg in { L where L is Subset of X : for K being Subset of X st K in C holds
L /\ K <> {} } or Lg in {0 } ) ) by A17, A19, XBOOLE_0:def 3;
A21: dom (Lg --> Lg) = Lg by FUNCOP_1:19;
A22: dom (Lf --> Lf) = Lf by FUNCOP_1:19;

per cases by A20, TARSKI:def 1;

suppose ( Lf in { L where L is Subset of X : for K being Subset of X st K in C holds
L /\ K <> {} } & Lg in { L where L is Subset of X : for K being Subset of X st K in C holds
L /\ K <> {} } ) ; :: thesis:

then consider Lff being Subset of X such that
A23: Lf = Lff and
A24: for K being Subset of X st K in C holds
Lff /\ K <> {} ;
A25: Lf /\ A <> {} by A14, A23, A24;
then consider a being set such that
A26: a in Lf /\ A by XBOOLE_0:def 1;
A27: ( a in Lf & a in A ) by A26, XBOOLE_0:def 4;
then A28: (f | A) . a = f . a by FUNCT_1:72
.= (Lf --> Lf) . a by A16, A22, A27, FUNCT_4:14
.= Lf by A27, FUNCOP_1:13 ;
A29: (g | A) . a = g . a by A27, FUNCT_1:72;
( g . a = 0 or g . a = Lg )

proof

per cases ;

suppose A30: a in Lg ; :: thesis:

then g . a = (Lg --> Lg) . a by A18, A21, FUNCT_4:14;
hence ( g . a = 0 or g . a = Lg ) by A30, FUNCOP_1:13; :: thesis:

end;

suppose not a in Lg ; :: thesis:

then g . a = (X --> 0 ) . a by A18, A21, FUNCT_4:12;
hence ( g . a = 0 or g . a = Lg ) by A26, FUNCOP_1:13; :: thesis:

end;

hence f | X = g | X by A15, A16, A18, A25, A28, A29; :: thesis:

end;

suppose A31: ( Lf in { L where L is Subset of X : for K being Subset of X st K in C holds
L /\ K <> {} } & Lg = 0 ) ; :: thesis:

then consider L being Subset of X such that
A32: Lf = L and
A33: for K being Subset of X st K in C holds
L /\ K <> {} ;
A34: Lf /\ A <> {} by A14, A32, A33;
then consider a being set such that
A35: a in Lf /\ A by XBOOLE_0:def 1;
A36: ( a in A & a in Lf ) by A35, XBOOLE_0:def 4;
A38: (g | A) . a = g . a by A36, FUNCT_1:72
.= ((X --> 0 ) +* {} ) . a by A18, A31
.= (X --> 0 ) . a by FUNCT_4:22
.= {} by A35, FUNCOP_1:13 ;
(f | A) . a = f . a by A36, FUNCT_1:72
.= (Lf --> Lf) . a by A16, A22, A36, FUNCT_4:14
.= Lf by A36, FUNCOP_1:13 ;
hence f | X = g | X by A15, A34, A38; :: thesis:

end;

suppose A39: ( Lf = 0 & Lg in { L where L is Subset of X : for K being Subset of X st K in C holds
L /\ K <> {} } ) ; :: thesis:

then consider L being Subset of X such that
A40: Lg = L and
A41: for K being Subset of X st K in C holds
L /\ K <> {} ;
A42: Lg /\ A <> {} by A14, A40, A41;
then consider a being set such that
A43: a in Lg /\ A by XBOOLE_0:def 1;
A44: ( a in A & a in Lg ) by A43, XBOOLE_0:def 4;
A46: (f | A) . a = f . a by A44, FUNCT_1:72
.= ((X --> 0 ) +* {} ) . a by A16, A39
.= (X --> 0 ) . a by FUNCT_4:22
.= {} by A43, FUNCOP_1:13 ;
(g | A) . a = g . a by A44, FUNCT_1:72
.= (Lg --> Lg) . a by A18, A21, A44, FUNCT_4:14
.= Lg by A44, FUNCOP_1:13 ;
hence f | X = g | X by A15, A42, A46; :: thesis:

end;

suppose ( Lf = 0 & Lg = 0 ) ; :: thesis:

hence f | X = g | X by A16, A18; :: thesis:

end;

then AA >|> XA,DB by Def8;
then [A,X] in Dependency-str DB ;
then consider a, b being Subset of X such that
A47: [a,b] in Maximal_wrt (Dependency-str DB) and
A48: [a,b] >= [A,([#] X)] by Th28;
A49: ( a c= A & X c= b ) by A48, Th15;
then A50: b = X by XBOOLE_0:def 10;
[a,b] in Dependency-str DB by A47;
then consider aa, XX being Subset of the Attributes of DB such that
A51: [a,b] = [aa,XX] and
A52: aa >|> XX,DB ;
A53: ( a = aa & b = XX ) by A51, ZFMISC_1:33;

now

assume A54: a <> A ; :: thesis:
set r0 = X --> 0 ;
set r1 = (X --> 0 ) +* ((a ` ) --> (a ` ));
0 in {0 } by TARSKI:def 1;
then 0 in M0 by XBOOLE_0:def 3;
then A55: (X --> 0 ) +* (({} X) --> ({} X)) in R ;

now

let K be Subset of X; :: thesis:
assume A56: K in C ; :: thesis:
assume (a ` ) /\ K = {} ; :: thesis:
then K misses a ` by XBOOLE_0:def 7;
then A57: K c= a by SUBSET_1:44;
then K c= A by A49, XBOOLE_1:1;
then K = A by A2, A14, A56, Def28;
hence contradiction by A49, A54, A57, XBOOLE_0:def 10; :: thesis:

end;

then a ` in { L where L is Subset of X : for K being Subset of X st K in C holds
L /\ K <> {} } ;
then a ` in M0 by XBOOLE_0:def 3;
then A58: (X --> 0 ) +* ((a ` ) --> (a ` )) in R ;
A59: dom ((a ` ) --> (a ` )) = a ` by FUNCOP_1:19;
reconsider r0 = X --> 0 , r1 = (X --> 0 ) +* ((a ` ) --> (a ` )) as Element of the Relationship of DB by A55, A58, FUNCT_4:22;

now

A60: dom (r0 | a) = (dom r0) /\ a by RELAT_1:90;
A61: dom r0 = X by FUNCOP_1:19;
dom r1 = (dom (X --> 0 )) \/ (dom ((a ` ) --> (a ` ))) by FUNCT_4:def 1
.= X \/ (dom ((a ` ) --> (a ` ))) by FUNCOP_1:19
.= X \/ (a ` ) by FUNCOP_1:19
.= X by XBOOLE_1:12 ;
hence dom (r0 | a) = (dom r1) /\ a by A61, RELAT_1:90; :: thesis:
let x be set ; :: thesis:
assume x in dom (r0 | a) ; :: thesis:
then A62: x in a by A60, XBOOLE_0:def 4;
a misses a ` by XBOOLE_1:79;
then a /\ (a ` ) = {} by XBOOLE_0:def 7;
then A63: not x in a ` by A62, XBOOLE_0:def 4;
thus (r0 | a) . x = (X --> 0 ) . x by A62, FUNCT_1:72
.= r1 . x by A59, A63, FUNCT_4:12 ; :: thesis:

end;

then A64: r0 | a = r1 | a by FUNCT_1:68;

A65: now

assume a ` = {} ; :: thesis:
then a ` c= a by XBOOLE_1:2;
then a = X by A12, SUBSET_1:39;
hence contradiction by A49, A54, XBOOLE_0:def 10; :: thesis:

end;

then consider y being set such that
A66: y in a ` by XBOOLE_0:def 1;
A67: (r0 | X) . y = r0 . y by A66, FUNCT_1:72
.= 0 by A66, FUNCOP_1:13 ;
(r1 | X) . y = r1 . y by A66, FUNCT_1:72
.= ((a ` ) --> (a ` )) . y by A59, A66, FUNCT_4:14
.= a ` by A66, FUNCOP_1:13 ;
hence contradiction by A50, A52, A53, A64, A65, A67, Def8; :: thesis:

end;

then [A,X] in Maximal_wrt (Dependency-str DB) by A47, A49, XBOOLE_0:def 10;
hence x in { A where A is Subset of X : [A,X] in Maximal_wrt (Dependency-str DB) } ; :: thesis:

end;

now

let x be set ; :: thesis:
thus ( x in C implies x in { A where A is Subset of X : [A,X] in Maximal_wrt (Dependency-str DB) } ) by A13; :: thesis:
assume x in { A where A is Subset of X : [A,X] in Maximal_wrt (Dependency-str DB) } ; :: thesis:
then consider A being Subset of X such that
A68: x = A and
A69: [A,X] in Maximal_wrt (Dependency-str DB) ;
A70: [A,X] in Dependency-str DB by A69;

A71: now

let K be set ; :: thesis:
assume that
A72: K in C and
A73: K c= A ; :: thesis:
K in { A where A is Subset of X : [A,X] in Maximal_wrt (Dependency-str DB) } by A13, A72;
then consider B being Subset of X such that
A74: K = B and
A75: [B,X] in Maximal_wrt (Dependency-str DB) ;
reconsider AA = A, B = B, XA = X as Subset of the Attributes of DB by A12;
assume A76: K <> A ; :: thesis:
A77: A ^|^ [#] X, Dependency-str DB by A69, Def18;
[AA,XA] <= [B,XA] by A73, A74, Th15;
hence contradiction by A74, A75, A76, A77, Th29; :: thesis:

end;

consider K being set such that
A78: K in C by A1, XBOOLE_0:def 1;
reconsider K = K as Subset of X by A78;
assume A79: not x in C ; :: thesis:
then not K c= A by A68, A71, A78;
then consider k being set such that
A80: ( k in K & not k in A ) by TARSKI:def 3;
set m = { a where a is Element of X : ( not a in A & ex K being set st
( K in C & a in K ) ) } ;
reconsider k = k as Element of X by A80;
A81: k in { a where a is Element of X : ( not a in A & ex K being set st
( K in C & a in K ) ) } by A78, A80;
then consider n being set such that
A82: n in { a where a is Element of X : ( not a in A & ex K being set st
( K in C & a in K ) ) } ;

now

let x be set ; :: thesis:
assume x in { a where a is Element of X : ( not a in A & ex K being set st
( K in C & a in K ) ) } ; :: thesis:
then ex a being Element of X st
( x = a & not a in A & ex K being set st
( K in C & a in K ) ) ;
hence x in X ; :: thesis:

end;

then reconsider m = { a where a is Element of X : ( not a in A & ex K being set st
( K in C & a in K ) ) } as Subset of X by TARSKI:def 3;

now

let K be Subset of X; :: thesis:
assume A83: K in C ; :: thesis:
not K c= A by A68, A71, A79, A83;
then consider k being set such that
A84: ( k in K & not k in A ) by TARSKI:def 3;
k in m by A83, A84;
hence m /\ K <> {} by A84, XBOOLE_0:def 4; :: thesis:

end;

then A85: m in { L where L is Subset of X : for K being Subset of X st K in C holds
L /\ K <> {} } ;
set r0 = X --> 0 ;
set r1 = (X --> 0 ) +* (m --> m);
0 in {0 } by TARSKI:def 1;
then 0 in M0 by XBOOLE_0:def 3;
then A86: (X --> 0 ) +* (({} X) --> ({} X)) in R ;
m in M0 by A85, XBOOLE_0:def 3;
then (X --> 0 ) +* (m --> m) in R ;
then reconsider r0 = X --> 0 , r1 = (X --> 0 ) +* (m --> m) as Element of the Relationship of DB by A86, FUNCT_4:22;
A87: dom (m --> m) = m by FUNCOP_1:19;

now

A88: dom (r0 | A) = (dom r0) /\ A by RELAT_1:90;
A89: dom r0 = X by FUNCOP_1:19;
dom r1 = (dom (X --> 0 )) \/ (dom (m --> m)) by FUNCT_4:def 1
.= X \/ (dom (m --> m)) by FUNCOP_1:19
.= X \/ m by FUNCOP_1:19
.= X by XBOOLE_1:12 ;
hence dom (r0 | A) = (dom r1) /\ A by A89, RELAT_1:90; :: thesis:
let x be set ; :: thesis:
assume A90: x in dom (r0 | A) ; :: thesis:
A91: x in A by A88, A90, XBOOLE_0:def 4;

A92: now

assume x in m ; :: thesis:
then ex a being Element of X st
( x = a & not a in A & ex K being set st
( K in C & a in K ) ) ;
hence contradiction by A88, A90, XBOOLE_0:def 4; :: thesis:

end;

thus (r0 | A) . x = (X --> 0 ) . x by A91, FUNCT_1:72
.= r1 . x by A87, A92, FUNCT_4:12 ; :: thesis:

end;

then A93: r0 | A = r1 | A by FUNCT_1:68;
consider aa, XX being Subset of the Attributes of DB such that
A94: [A,X] = [aa,XX] and
A95: aa >|> XX,DB by A70;
A96: ( A = aa & X = XX ) by A94, ZFMISC_1:33;
A97: m c= X ;
then A98: (r0 | X) . n = r0 . n by A82, FUNCT_1:72
.= 0 by A82, A97, FUNCOP_1:13 ;
(r1 | X) . n = r1 . n by A82, FUNCT_1:72
.= (m --> m) . n by A82, A87, FUNCT_4:14
.= m by A82, FUNCOP_1:13 ;
hence contradiction by A81, A93, A95, A96, A98, Def8; :: thesis:

end;

hence C = candidate-keys (Dependency-str DB) by TARSKI:2; :: thesis: