let A be non empty finite set ; for F being Dependency-set of A holds
( ( for A, B being Subset of A holds
( [A,B] in Dependency-closure F iff for a being Subset of A st A c= a & not B c= a holds
a in charact_set F ) ) & saturated-subsets (Dependency-closure F) = (bool A) \ (charact_set F) )
let F be Dependency-set of A; ( ( for A, B being Subset of A holds
( [A,B] in Dependency-closure F iff for a being Subset of A st A c= a & not B c= a holds
a in charact_set F ) ) & saturated-subsets (Dependency-closure F) = (bool A) \ (charact_set F) )
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 } ;
now for c being object holds
( ( c in (bool A) \ (charact_set F) implies 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 } ) & ( 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 } implies c in (bool A) \ (charact_set F) ) )let c be
object ;
( ( c in (bool A) \ (charact_set F) implies 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 } ) & ( 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 } implies c in (bool A) \ (charact_set F) ) )reconsider cc =
c as
set by TARSKI:1;
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 }
;
c in (bool A) \ (charact_set F)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;
verum 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;
hereby saturated-subsets (Dependency-closure F) = (bool A) \ (charact_set F)
let X,
Y be
Subset of
A;
( ( [X,Y] in Dependency-closure F implies for a being Subset of A st X c= a & not Y c= a holds
a in charact_set F ) & ( ( for a being Subset of A st X c= a & not Y c= a holds
a in charact_set F ) implies [X,Y] in Dependency-closure F ) )hereby ( ( for a being Subset of A st X c= a & not Y c= a holds
a in charact_set F ) implies [X,Y] in Dependency-closure F )
assume
[X,Y] in Dependency-closure F
;
for a being Subset of A st X c= a & not Y c= a holds
a in charact_set Fthen
[X,Y] in FF
by A10;
then consider a9,
b9 being
Subset of
A such that A11:
[a9,b9] = [X,Y]
and A12:
for
c being
set st
c in B &
a9 c= c holds
b9 c= c
;
A13:
b9 = Y
by A11, XTUPLE_0:1;
let a be
Subset of
A;
( X c= a & not Y c= a implies a in charact_set F )assume that A14:
X c= a
and A15:
not
Y c= a
;
a in charact_set Fassume
not
a in charact_set F
;
contradictionthen A16:
a in B
by XBOOLE_0:def 5;
a9 = X
by A11, XTUPLE_0:1;
hence
contradiction
by A14, A15, A12, A13, A16;
verum
end; assume A17:
for
a being
Subset of
A st
X c= a & not
Y c= a holds
a in charact_set F
;
[X,Y] in Dependency-closure Fthen
[X,Y] in FF
;
hence
[X,Y] in Dependency-closure F
by A8;
verum
end;
for x, y being Subset of A st [x,y] in F & x c= A holds
y c= A
;
then
not [#] A in charact_set F
by Th55;
then
A in B
by XBOOLE_0:def 5;
then A21:
B is (B1)
;
Dependency-closure F = FF
by A10, A8, XBOOLE_0:def 10;
hence
saturated-subsets (Dependency-closure F) = (bool A) \ (charact_set F)
by A21, A6, A7, Th35; verum