let X be non empty finite set ; :: thesis: for G being Subset-Family of X holds G is_generator-set_of saturated-subsets (X deps_encl_by G)
let G be Subset-Family of X; :: thesis: G is_generator-set_of saturated-subsets (X deps_encl_by G)
set F = X deps_encl_by G;
set ssF = saturated-subsets (X deps_encl_by G);
X deps_encl_by G is full_family by Th35;
then A1: ( saturated-subsets (X deps_encl_by G) is (B1) & saturated-subsets (X deps_encl_by G) is (B2) ) by Th34;
thus G is_generator-set_of saturated-subsets (X deps_encl_by G) :: thesis: verum

proof

thus A2: G c= saturated-subsets (X deps_encl_by G) by Th36; :: according to ARMSTRNG:def 26 :: thesis: saturated-subsets (X deps_encl_by G) = { (Intersect S) where S is Subset-Family of X : S c= G }
set H = { (Intersect S) where S is Subset-Family of X : S c= G } ;

now

let x be set ; :: thesis: ( ( x in saturated-subsets (X deps_encl_by G) implies x in { (Intersect S) where S is Subset-Family of X : S c= G } ) & ( x in { (Intersect S) where S is Subset-Family of X : S c= G } implies x in saturated-subsets (X deps_encl_by G) ) )

hereby :: thesis: ( x in { (Intersect S) where S is Subset-Family of X : S c= G } implies x in saturated-subsets (X deps_encl_by G) )

assume x in saturated-subsets (X deps_encl_by G) ; :: thesis: x in { (Intersect S) where S is Subset-Family of X : S c= G }
then consider b', a' being Subset of X such that
A3: x = b' and
A4: a' ^|^ b',X deps_encl_by G by Th33;
[a',b'] in Maximal_wrt (X deps_encl_by G) by A4, Def18;
then [a',b'] in X deps_encl_by G ;
then consider a, b being Subset of X such that
A5: [a,b] = [a',b'] and
A6: for c being set st c in G & a c= c holds
b c= c ;
A7: ( a = a' & b = b' ) by A5, ZFMISC_1:33;
set C = { c where c is Subset of X : ( c in G & a c= c ) } ;
{ c where c is Subset of X : ( c in G & a c= c ) } c= bool X

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { c where c is Subset of X : ( c in G & a c= c ) } or x in bool X )
assume x in { c where c is Subset of X : ( c in G & a c= c ) } ; :: thesis: x in bool X
then ex c being Subset of X st
( x = c & c in G & a c= c ) ;
hence x in bool X ; :: thesis: verum

end;

then reconsider C = { c where c is Subset of X : ( c in G & a c= c ) } as Subset-Family of X ;
set ic = Intersect C;

now

let z1 be set ; :: thesis: ( z1 in C implies b c= z1 )
assume z1 in C ; :: thesis: b c= z1
then consider c being Subset of X such that
A8: ( z1 = c & c in G & a c= c ) ;
thus b c= z1 by A6, A8; :: thesis: verum

end;

then A9: b c= Intersect C by MSSUBFAM:4;
A10: C c= G

proof

let c be set ; :: according to TARSKI:def 3 :: thesis: ( not c in C or c in G )
assume c in C ; :: thesis: c in G
then ex cc being Subset of X st
( cc = c & cc in G & a c= cc ) ;
hence c in G ; :: thesis: verum

end;

thus x in { (Intersect S) where S is Subset-Family of X : S c= G } :: thesis: verum

proof

per cases ( b = Intersect C or b <> Intersect C ) ;

suppose b = Intersect C ; :: thesis: x in { (Intersect S) where S is Subset-Family of X : S c= G }

hence x in { (Intersect S) where S is Subset-Family of X : S c= G } by A3, A7, A10; :: thesis: verum

end;

suppose A11: b <> Intersect C ; :: thesis: x in { (Intersect S) where S is Subset-Family of X : S c= G }

reconsider ic = Intersect C as Subset of X ;

now

let c be set ; :: thesis: ( c in G & a c= c implies ic c= c )
assume ( c in G & a c= c ) ; :: thesis: ic c= c
then c in C ;
hence ic c= c by MSSUBFAM:2; :: thesis: verum

end;

then A12: [a,ic] in X deps_encl_by G ;
[a,b] <= [a,ic] by A9, Th15;
hence x in { (Intersect S) where S is Subset-Family of X : S c= G } by A4, A7, A11, A12, Th29; :: thesis: verum

end;

end;

end;

end;

assume x in { (Intersect S) where S is Subset-Family of X : S c= G } ; :: thesis: x in saturated-subsets (X deps_encl_by G)
then consider S being Subset-Family of X such that
A13: Intersect S = x and
A14: S c= G ;
X in saturated-subsets (X deps_encl_by G) by A1, Def4;
hence x in saturated-subsets (X deps_encl_by G) by A1, A2, A13, A14, Th1, XBOOLE_1:1; :: thesis: verum

end;

hence saturated-subsets (X deps_encl_by G) = { (Intersect S) where S is Subset-Family of X : S c= G } by TARSKI:2; :: thesis: verum

end;