let A be non empty finite set ; :: thesis:
let F be Dependency-set of A; :: thesis:
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 } ;

let c be object ; :: thesis:
reconsider cc = c as set by TARSKI:1;

assume A1: c in (bool A) \ (charact_set F) ; :: thesis:
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:

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

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;

let X, Y be Subset of A; :: thesis:

end;

end;

end;