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