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;
A1: F c= Dependency-closure F by Def25;
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

let c be set ; :: 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) ) )

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 A2: 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 ( c in bool A & 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= c holds
y c= c ;
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 A2; :: 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
A3: c = b and
A4: 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 A4, Th57;
hence c in (bool A) \ (charact_set F) by A3, XBOOLE_0:def 5; :: thesis: verum

end;

then A5: (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 ;
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 Th57;
then A in B by XBOOLE_0:def 5;
then A6: B is (B1) by Def4;
A7: { 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 A8: B is (B2) by A5, Th38;
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 } ;
A9: { [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 ;
A10: FF is full_family by A9, Th35;
F c= FF by A5, A7, A9, Th39;
then A11: Dependency-closure F c= FF by A10, Def25;
A12: FF c= Dependency-closure F by A1, A5, A7, A9, Th39;
then A13: Dependency-closure F = FF by A11, XBOOLE_0:def 10;

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 A14: [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
let a be Subset of A; :: thesis: ( X c= a & not Y c= a implies a in charact_set F )
assume A15: ( X c= a & not Y c= a ) ; :: thesis: a in charact_set F
[X,Y] in FF by A11, A14;
then consider a', b' being Subset of A such that
A16: [a',b'] = [X,Y] and
A17: for c being set st c in B & a' c= c holds
b' c= c ;
A18: ( a' = X & b' = Y ) by A16, ZFMISC_1:33;
assume not a in charact_set F ; :: thesis: contradiction
then a in B by XBOOLE_0:def 5;
hence contradiction by A15, A17, A18; :: thesis: verum

end;

assume A19: 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

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

end;

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

end;

thus saturated-subsets (Dependency-closure F) = (bool A) \ (charact_set F) by A6, A8, A9, A13, Th37; :: thesis: verum