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 :: thesis: for A being object holds
( ( 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 ) )

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 } ;
let A be object ; :: 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 ) )
reconsider AA = A as set by TARSKI:1;

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

A1: F c= Dependency-closure F by Def24;
assume A2: A in charact_set F ; :: thesis: A in charact_set (Dependency-closure F)
then A3: A is Subset of X by Th55;
ex x, y being Subset of X st
( [x,y] in F & x c= AA & not y c= AA ) by A2, Th55;
hence A in charact_set (Dependency-closure F) by A1, 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= AA and
A7: not y c= AA by Th55;
A8: A is Subset of X by A4, Th55;
assume not A in charact_set F ; :: thesis: contradiction
then for x, y being Subset of X st [x,y] in F & x c= AA holds
y c= AA by A8;
then A9: 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 A8;
{ 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 Th38;
then consider a, b being Subset of X such that
A10: [x,y] = [a,b] and
A11: 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;
A12: y = b by A10, XTUPLE_0:1;
x = a by A10, XTUPLE_0:1;
hence contradiction by A6, A7, A11, A12, A9; :: thesis: verum

end;

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