let X be non empty finite set ; :: thesis: for B being Subset-Family of X holds B c= saturated-subsets (X deps_encl_by B)
let B be Subset-Family of X; :: thesis: B c= saturated-subsets (X deps_encl_by B)
set F = X deps_encl_by B;
set ss = saturated-subsets (X deps_encl_by B);
reconsider F' = X deps_encl_by B as Full-family of X by Th35;
set M = Maximal_wrt F';
A1: Maximal_wrt F' is (M1) by Th30;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in B or x in saturated-subsets (X deps_encl_by B) )
assume A2: x in B ; :: thesis: x in saturated-subsets (X deps_encl_by B)
then reconsider x' = x as Element of B ;
reconsider x'' = x as Subset of X by A2;
consider a', b' being Subset of X such that
A3: [a',b'] >= [x'',x''] and
A4: [a',b'] in Maximal_wrt F' by A1, Def19;
A5: ( a' c= x'' & x'' c= b' ) by A3, Th15;
[a',b'] in X deps_encl_by B by A4;
then consider a, b being Subset of X such that
A6: [a',b'] = [a,b] and
A7: for c being set st c in B & a c= c holds
b c= c ;
A8: ( a' = a & b' = b ) by A6, ZFMISC_1:33;
then b c= x' by A2, A5, A7;
then A9: b = x by A5, A8, XBOOLE_0:def 10;
a ^|^ b,X deps_encl_by B by A4, A6, Def18;
hence x in saturated-subsets (X deps_encl_by B) by A9; :: thesis: verum