let X be non empty finite set ; :: thesis: for F being Dependency-set of X holds charact_set F = charact_set (Dependency-closure F)
let F be Dependency-set of X; :: thesis: charact_set F = charact_set (Dependency-closure F)
set dcF = Dependency-closure F;

now

let A be set ; :: thesis: ( ( A in charact_set F implies A in charact_set (Dependency-closure F) ) & ( A in charact_set (Dependency-closure F) implies A in charact_set F ) )

hereby :: thesis: ( A in charact_set (Dependency-closure F) implies A in charact_set F )

assume A1: A in charact_set F ; :: thesis: A in charact_set (Dependency-closure F)
then consider x, y being Subset of X such that
A2: [x,y] in F and
A3: ( x c= A & not y c= A ) by Th57;
F c= Dependency-closure F by Def25;
then ( A is Subset of X & [x,y] in Dependency-closure F ) by A1, A2, Th57;
hence A in charact_set (Dependency-closure F) by A3; :: thesis: verum

end;

assume A4: A in charact_set (Dependency-closure F) ; :: thesis: A in charact_set F
then consider x, y being Subset of X such that
A5: [x,y] in Dependency-closure F and
A6: ( x c= A & not y c= A ) by Th57;
A7: A is Subset of X by A4, Th57;
assume not A in charact_set F ; :: thesis: contradiction
then A8: for x, y being Subset of X st [x,y] in F & x c= A holds
y c= A by A7;
set B = { c where c is Subset of X : for x, y being Subset of X st [x,y] in F & x c= c holds
y c= c } ;
{ c where c is Subset of X : for x, y being Subset of X st [x,y] in F & x c= c holds
y c= c } = enclosure_of F ;
then Dependency-closure F = X deps_encl_by { c where c is Subset of X : for x, y being Subset of X st [x,y] in F & x c= c holds
y c= c } by Th40;
then consider a, b being Subset of X such that
A9: [x,y] = [a,b] and
A10: for c being set st c in { c where c is Subset of X : for x, y being Subset of X st [x,y] in F & x c= c holds
y c= c } & a c= c holds
b c= c by A5;
A11: ( x = a & y = b ) by A9, ZFMISC_1:33;
A in { c where c is Subset of X : for x, y being Subset of X st [x,y] in F & x c= c holds
y c= c } by A7, A8;
hence contradiction by A6, A10, A11; :: thesis: verum

end;

hence charact_set F = charact_set (Dependency-closure F) by TARSKI:2; :: thesis: verum