let X be non empty finite set ; for F being Dependency-set of X holds charact_set F = charact_set (Dependency-closure F)
let F be Dependency-set of X; charact_set F = charact_set (Dependency-closure F)
set dcF = Dependency-closure F;
now 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 ;
( ( 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)
;
A in charact_set Fthen 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
;
contradictionthen
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;
verum end;
hence
charact_set F = charact_set (Dependency-closure F)
by TARSKI:2; verum