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