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;
reconsider F9 = X deps_encl_by B as Full-family of X by Th33;
set M = Maximal_wrt F9;
let x be object ; :: 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 x9 = x as Element of B ;
reconsider x99 = x as Subset of X by A1;
Maximal_wrt F9 is (M1) by Th28;
then consider a9, b9 being Subset of X such that
A2: [a9,b9] >= [x99,x99] and
A3: [a9,b9] in Maximal_wrt F9 ;
A4: a9 c= x99 by A2;
[a9,b9] in X deps_encl_by B by A3;
then consider a, b being Subset of X such that
A5: [a9,b9] = [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;
a9 = a by A5, XTUPLE_0:1;
then A8: b c= x9 by A1, A4, A6;
A9: b9 = b by A5, XTUPLE_0:1;
x99 c= b9 by A2;
then b = x by A9, A8, XBOOLE_0:def 10;
hence x in saturated-subsets (X deps_encl_by B) by A7; :: thesis: verum