let X be non empty finite set ; :: thesis: for F being Full-family of X ex G being Subset-Family of X st
( G is_generator-set_of saturated-subsets F & F = X deps_encl_by G )
let F be Full-family of X; :: thesis: ex G being Subset-Family of X st
( G is_generator-set_of saturated-subsets F & F = X deps_encl_by G )
set G = saturated-subsets F;
take saturated-subsets F ; :: thesis: ( saturated-subsets F is_generator-set_of saturated-subsets F & F = X deps_encl_by (saturated-subsets F) )
A1: ( saturated-subsets F is (B1) & saturated-subsets F is (B2) ) by Th32;
thus saturated-subsets F is_generator-set_of saturated-subsets F :: thesis: F = X deps_encl_by (saturated-subsets F)
proof
set H = { (Intersect S) where S is Subset-Family of X : S c= saturated-subsets F } ;
thus saturated-subsets F c= saturated-subsets F ; :: according to ARMSTRNG:def 25 :: thesis: saturated-subsets F = { (Intersect S) where S is Subset-Family of X : S c= saturated-subsets F }
now :: thesis: for x being object holds
( ( x in saturated-subsets F implies x in { (Intersect S) where S is Subset-Family of X : S c= saturated-subsets F } ) & ( x in { (Intersect S) where S is Subset-Family of X : S c= saturated-subsets F } implies x in saturated-subsets F ) )
let x be object ; :: thesis: ( ( x in saturated-subsets F implies x in { (Intersect S) where S is Subset-Family of X : S c= saturated-subsets F } ) & ( x in { (Intersect S) where S is Subset-Family of X : S c= saturated-subsets F } implies x in saturated-subsets F ) )
hereby :: thesis: ( x in { (Intersect S) where S is Subset-Family of X : S c= saturated-subsets F } implies x in saturated-subsets F )
reconsider xx = x as set by TARSKI:1;
set sx = {xx};
assume A2: x in saturated-subsets F ; :: thesis: x in { (Intersect S) where S is Subset-Family of X : S c= saturated-subsets F }
then A3: {xx} c= saturated-subsets F by ZFMISC_1:31;
reconsider sx = {xx} as Subset-Family of X by A2, ZFMISC_1:31;
A4: Intersect sx = meet sx by SETFAM_1:def 9;
Intersect sx in { (Intersect S) where S is Subset-Family of X : S c= saturated-subsets F } by A3;
hence x in { (Intersect S) where S is Subset-Family of X : S c= saturated-subsets F } by A4, SETFAM_1:10; :: thesis: verum
end;
assume x in { (Intersect S) where S is Subset-Family of X : S c= saturated-subsets F } ; :: thesis: x in saturated-subsets F
then A5: ex S being Subset-Family of X st
( Intersect S = x & S c= saturated-subsets F ) ;
thus x in saturated-subsets F by A1, A5, Th1; :: thesis: verum
end;
hence saturated-subsets F = { (Intersect S) where S is Subset-Family of X : S c= saturated-subsets F } by TARSKI:2; :: thesis: verum
end;
thus F = X deps_encl_by (saturated-subsets F) by A1, Th35; :: thesis: verum