let X be non empty finite set ; :: thesis: for F being Dependency-set of X holds
( F c= X deps_encl_by (enclosure_of F) & ( for G being Dependency-set of X st F c= G & G is full_family holds
X deps_encl_by (enclosure_of F) c= G ) )
let F be Dependency-set of X; :: thesis: ( F c= X deps_encl_by (enclosure_of F) & ( for G being Dependency-set of X st F c= G & G is full_family holds
X deps_encl_by (enclosure_of F) c= G ) )
set B = enclosure_of F;
set H = X deps_encl_by (enclosure_of F);
thus F c= X deps_encl_by (enclosure_of F) :: thesis: for G being Dependency-set of X st F c= G & G is full_family holds
X deps_encl_by (enclosure_of F) c= G

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in F or x in X deps_encl_by (enclosure_of F) )
assume A1: x in F ; :: thesis: x in X deps_encl_by (enclosure_of F)
then consider a, b being Subset of X such that
A2: x = [a,b] by Th10;

now

let c be set ; :: thesis: ( c in enclosure_of F & a c= c implies b c= c )
assume that
A3: c in enclosure_of F and
A4: a c= c and
A5: not b c= c ; :: thesis: contradiction
reconsider c = c as Subset of X by A3;
ex c' being Subset of X st
( c' = c & ( for x, y being Subset of X st [x,y] in F & x c= c' holds
y c= c' ) ) by A3;
hence contradiction by A1, A2, A4, A5; :: thesis: verum

end;

hence x in X deps_encl_by (enclosure_of F) by A2; :: thesis: verum

end;

let G be Dependency-set of X; :: thesis: ( F c= G & G is full_family implies X deps_encl_by (enclosure_of F) c= G )
assume that
A6: F c= G and
A7: G is full_family ; :: thesis: X deps_encl_by (enclosure_of F) c= G
let z be set ; :: according to TARSKI:def 3 :: thesis: ( not z in X deps_encl_by (enclosure_of F) or z in G )
assume z in X deps_encl_by (enclosure_of F) ; :: thesis: z in G
then consider a, b being Subset of X such that
A8: z = [a,b] and
A9: for c being set st c in enclosure_of F & a c= c holds
b c= c ;
( enclosure_of F is (B1) & enclosure_of F is (B2) ) by Th38;
then A10: enclosure_of F = saturated-subsets (X deps_encl_by (enclosure_of F)) by Th37;
set B' = saturated-subsets G;
A11: ( saturated-subsets G is (B1) & saturated-subsets G is (B2) ) by A7, Th34;
set GG = { [e,f] where e, f is Subset of X : for c being set st c in saturated-subsets G & e c= c holds
f c= c } ;
{ [e,f] where e, f is Subset of X : for c being set st c in saturated-subsets G & e c= c holds
f c= c } = X deps_encl_by (saturated-subsets G) ;
then A12: { [e,f] where e, f is Subset of X : for c being set st c in saturated-subsets G & e c= c holds
f c= c } = G by A7, A11, Th37;
saturated-subsets G c= saturated-subsets (X deps_encl_by (enclosure_of F))

proof

let d be set ; :: according to TARSKI:def 3 :: thesis: ( not d in saturated-subsets G or d in saturated-subsets (X deps_encl_by (enclosure_of F)) )
assume that
A13: d in saturated-subsets G and
A14: not d in saturated-subsets (X deps_encl_by (enclosure_of F)) ; :: thesis: contradiction
reconsider d = d as Subset of X by A13;
consider x, y being Subset of X such that
A15: [x,y] in F and
A16: x c= d and
A17: not y c= d by A10, A14;
[x,y] in G by A6, A15;
then consider e, f being Subset of X such that
A18: [x,y] = [e,f] and
A19: for c being set st c in saturated-subsets G & e c= c holds
f c= c by A12;
( x = e & y = f ) by A18, ZFMISC_1:33;
hence contradiction by A13, A16, A17, A19; :: thesis: verum

end;

then for c being set st c in saturated-subsets G & a c= c holds
b c= c by A9, A10;
hence z in G by A8, A12; :: thesis: verum