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 object ; :: 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 Th9;

now :: thesis: for c being set st c in enclosure_of F & a c= c holds
b c= c

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 c9 being Subset of X st
( c9 = c & ( for x, y being Subset of X st [x,y] in F & x c= c9 holds
y c= c9 ) ) 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
set B9 = saturated-subsets G;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in X deps_encl_by (enclosure_of F) or z in G )
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 } ;
A8: { [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) ;
( enclosure_of F is (B1) & enclosure_of F is (B2) ) by Th36;
then A9: enclosure_of F = saturated-subsets (X deps_encl_by (enclosure_of F)) by Th35;
assume z in X deps_encl_by (enclosure_of F) ; :: thesis: z in G
then consider a, b being Subset of X such that
A10: z = [a,b] and
A11: for c being set st c in enclosure_of F & a c= c holds
b c= c ;
( saturated-subsets G is (B1) & saturated-subsets G is (B2) ) by A7, Th32;
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, A8, Th35;
saturated-subsets G c= saturated-subsets (X deps_encl_by (enclosure_of F))

proof

let d be object ; :: 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 A9, 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;
A20: y = f by A18, XTUPLE_0:1;
x = e by A18, XTUPLE_0:1;
hence contradiction by A13, A16, A17, A19, A20; :: thesis: verum

end;

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