let A be non empty finite set ; :: thesis: for F being Dependency-set of A holds
( ( for A, B being Subset of A holds
( [A,B] in Dependency-closure F iff for a being Subset of A st A c= a & not B c= a holds
a in charact_set F ) ) & saturated-subsets (Dependency-closure F) = (bool A) \ (charact_set F) )
let F be Dependency-set of A; :: thesis: ( ( for A, B being Subset of A holds
( [A,B] in Dependency-closure F iff for a being Subset of A st A c= a & not B c= a holds
a in charact_set F ) ) & saturated-subsets (Dependency-closure F) = (bool A) \ (charact_set F) )
set G = Dependency-closure F;
set B = (bool A) \ (charact_set F);
set BB = { b where b is Subset of A : for x, y being Subset of A st [x,y] in F & x c= b holds
y c= b } ;

now :: thesis: for c being object holds
( ( c in (bool A) \ (charact_set F) implies c in { b where b is Subset of A : for x, y being Subset of A st [x,y] in F & x c= b holds
y c= b } ) & ( c in { b where b is Subset of A : for x, y being Subset of A st [x,y] in F & x c= b holds
y c= b } implies c in (bool A) \ (charact_set F) ) )

let c be object ; :: thesis: ( ( c in (bool A) \ (charact_set F) implies c in { b where b is Subset of A : for x, y being Subset of A st [x,y] in F & x c= b holds
y c= b } ) & ( c in { b where b is Subset of A : for x, y being Subset of A st [x,y] in F & x c= b holds
y c= b } implies c in (bool A) \ (charact_set F) ) )
reconsider cc = c as set by TARSKI:1;

hereby :: thesis: ( c in { b where b is Subset of A : for x, y being Subset of A st [x,y] in F & x c= b holds
y c= b } implies c in (bool A) \ (charact_set F) )

assume A1: c in (bool A) \ (charact_set F) ; :: thesis: c in { b where b is Subset of A : for x, y being Subset of A st [x,y] in F & x c= b holds
y c= b }
then not c in charact_set F by XBOOLE_0:def 5;
then for x, y being Subset of A st [x,y] in F & x c= cc holds
y c= cc by A1;
hence c in { b where b is Subset of A : for x, y being Subset of A st [x,y] in F & x c= b holds
y c= b } by A1; :: thesis: verum

end;

assume c in { b where b is Subset of A : for x, y being Subset of A st [x,y] in F & x c= b holds
y c= b } ; :: thesis: c in (bool A) \ (charact_set F)
then consider b being Subset of A such that
A2: c = b and
A3: for x, y being Subset of A st [x,y] in F & x c= b holds
y c= b ;
not b in charact_set F by A3, Th55;
hence c in (bool A) \ (charact_set F) by A2, XBOOLE_0:def 5; :: thesis: verum

end;

then A4: (bool A) \ (charact_set F) = { b where b is Subset of A : for x, y being Subset of A st [x,y] in F & x c= b holds
y c= b } by TARSKI:2;
reconsider B = (bool A) \ (charact_set F) as Subset-Family of A ;
A5: { b where b is Subset of A : for x, y being Subset of A st [x,y] in F & x c= b holds
y c= b } = enclosure_of F ;
then A6: B is (B2) by A4, Th36;
set FF = { [a,b] where a, b is Subset of A : for c being set st c in B & a c= c holds
b c= c } ;
A7: { [a,b] where a, b is Subset of A : for c being set st c in B & a c= c holds
b c= c } = A deps_encl_by B ;
then reconsider FF = { [a,b] where a, b is Subset of A : for c being set st c in B & a c= c holds
b c= c } as Dependency-set of A ;
F c= Dependency-closure F by Def24;
then A8: FF c= Dependency-closure F by A4, A5, A7, Th37;
A9: FF is full_family by A7, Th33;
F c= FF by A4, A5, A7, Th37;
then A10: Dependency-closure F c= FF by A9, Def24;

hereby :: thesis: saturated-subsets (Dependency-closure F) = (bool A) \ (charact_set F)

let X, Y be Subset of A; :: thesis: ( ( [X,Y] in Dependency-closure F implies for a being Subset of A st X c= a & not Y c= a holds
a in charact_set F ) & ( ( for a being Subset of A st X c= a & not Y c= a holds
a in charact_set F ) implies [X,Y] in Dependency-closure F ) )

hereby :: thesis: ( ( for a being Subset of A st X c= a & not Y c= a holds
a in charact_set F ) implies [X,Y] in Dependency-closure F )

assume [X,Y] in Dependency-closure F ; :: thesis: for a being Subset of A st X c= a & not Y c= a holds
a in charact_set F
then [X,Y] in FF by A10;
then consider a9, b9 being Subset of A such that
A11: [a9,b9] = [X,Y] and
A12: for c being set st c in B & a9 c= c holds
b9 c= c ;
A13: b9 = Y by A11, XTUPLE_0:1;
let a be Subset of A; :: thesis: ( X c= a & not Y c= a implies a in charact_set F )
assume that
A14: X c= a and
A15: not Y c= a ; :: thesis: a in charact_set F
assume not a in charact_set F ; :: thesis: contradiction
then A16: a in B by XBOOLE_0:def 5;
a9 = X by A11, XTUPLE_0:1;
hence contradiction by A14, A15, A12, A13, A16; :: thesis: verum

end;

assume A17: for a being Subset of A st X c= a & not Y c= a holds
a in charact_set F ; :: thesis: [X,Y] in Dependency-closure F

now :: thesis: for c being set st c in B & X c= c holds
Y c= c

let c be set ; :: thesis: ( c in B & X c= c implies Y c= c )
assume that
A18: c in B and
A19: X c= c and
A20: not Y c= c ; :: thesis: contradiction
reconsider c = c as Subset of A by A18;
not c in charact_set F by A18, XBOOLE_0:def 5;
hence contradiction by A17, A19, A20; :: thesis: verum

end;

then [X,Y] in FF ;
hence [X,Y] in Dependency-closure F by A8; :: thesis: verum

end;

for x, y being Subset of A st [x,y] in F & x c= A holds
y c= A ;
then not [#] A in charact_set F by Th55;
then A in B by XBOOLE_0:def 5;
then A21: B is (B1) ;
Dependency-closure F = FF by A10, A8, XBOOLE_0:def 10;
hence saturated-subsets (Dependency-closure F) = (bool A) \ (charact_set F) by A21, A6, A7, Th35; :: thesis: verum