let X be non empty finite set ; :: thesis: for B being Subset-Family of X st B is (B1) & B is (B2) holds
( B = saturated-subsets (X deps_encl_by B) & ( for G being Full-family of X st B = saturated-subsets G holds
G = X deps_encl_by B ) )
let B be Subset-Family of X; :: thesis: ( B is (B1) & B is (B2) implies ( B = saturated-subsets (X deps_encl_by B) & ( for G being Full-family of X st B = saturated-subsets G holds
G = X deps_encl_by B ) ) )
assume A1: ( B is (B1) & B is (B2) ) ; :: thesis: ( B = saturated-subsets (X deps_encl_by B) & ( for G being Full-family of X st B = saturated-subsets G holds
G = 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';
A2: X in B by A1, Def4;
reconsider B' = B as non empty set by A1, Def4;

now

let x be set ; :: thesis: ( ( x in B implies x in saturated-subsets (X deps_encl_by B) ) & ( x in saturated-subsets (X deps_encl_by B) implies x in B ) )
B c= saturated-subsets (X deps_encl_by B) by Th36;
hence ( x in B implies x in saturated-subsets (X deps_encl_by B) ) ; :: thesis: ( x in saturated-subsets (X deps_encl_by B) implies x in B )
assume x in saturated-subsets (X deps_encl_by B) ; :: thesis: x in B
then consider b, a being Subset of X such that
A3: x = b and
A4: a ^|^ b,X deps_encl_by B by Th33;
[a,b] in Maximal_wrt F' by A4, Def18;
then [a,b] in X deps_encl_by B ;
then consider aa, bb being Subset of X such that
A5: [a,b] = [aa,bb] and
A6: for c being set st c in B & aa c= c holds
bb c= c ;
A7: ( a = aa & b = bb ) by A5, ZFMISC_1:33;
set S = { b' where b' is Element of B' : a c= b' } ;
A9: { b' where b' is Element of B' : a c= b' } c= bool X

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { b' where b' is Element of B' : a c= b' } or x in bool X )
assume x in { b' where b' is Element of B' : a c= b' } ; :: thesis: x in bool X
then consider b' being Element of B' such that
A10: ( x = b' & a c= b' ) ;
( b' in B' & B c= bool X ) ;
hence x in bool X by A10; :: thesis: verum

end;

A12: X in { b' where b' is Element of B' : a c= b' } by A2;
A13: { b' where b' is Element of B' : a c= b' } c= B

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { b' where b' is Element of B' : a c= b' } or x in B )
assume x in { b' where b' is Element of B' : a c= b' } ; :: thesis: x in B
then consider b' being Element of B' such that
A14: ( x = b' & a c= b' ) ;
thus x in B by A14; :: thesis: verum

end;

reconsider S = { b' where b' is Element of B' : a c= b' } as Subset-Family of X by A9;
set mS = Intersect S;
reconsider mS = Intersect S as Subset of X ;
A15: b c= mS

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in b or x in mS )
assume A16: x in b ; :: thesis: x in mS

now

let Y be set ; :: thesis: ( Y in S implies x in Y )
assume Y in S ; :: thesis: x in Y
then consider b' being Element of B' such that
A17: ( Y = b' & a c= b' ) ;
b c= b' by A6, A7, A17;
hence x in Y by A16, A17; :: thesis: verum

end;

then x in meet S by A12, SETFAM_1:def 1;
hence x in mS by A12, SETFAM_1:def 10; :: thesis: verum

end;

now

assume A18: b <> mS ; :: thesis: contradiction

now

let c be set ; :: thesis: ( c in B & a c= c implies mS c= c )
assume ( c in B & a c= c ) ; :: thesis: mS c= c
then c in S ;
then meet S c= c by SETFAM_1:4;
hence mS c= c by A12, SETFAM_1:def 10; :: thesis: verum

end;

then A19: [a,mS] in X deps_encl_by B ;
[a,mS] >= [a,b] by A15, Th15;
hence contradiction by A4, A18, A19, Th29; :: thesis: verum

end;

hence x in B by A1, A2, A3, A13, Th1; :: thesis: verum

end;

hence B = saturated-subsets (X deps_encl_by B) by TARSKI:2; :: thesis: for G being Full-family of X st B = saturated-subsets G holds
G = X deps_encl_by B
let G be Full-family of X; :: thesis: ( B = saturated-subsets G implies G = X deps_encl_by B )
assume A20: B = saturated-subsets G ; :: thesis: G = X deps_encl_by B
set MG = Maximal_wrt G;
A21: ( Maximal_wrt G is (M1) & Maximal_wrt G is (M3) ) by Th30;

now

let x be set ; :: thesis: ( ( x in G implies x in X deps_encl_by B ) & ( x in X deps_encl_by B implies x in G ) )

hereby :: thesis: ( x in X deps_encl_by B implies x in G )

assume x in G ; :: thesis: x in X deps_encl_by B
then reconsider x1 = x as Element of G ;
reconsider x' = x1 as Dependency of X ;
consider a, b being Subset of X such that
A22: x' = [a,b] by Th9;

now

let b' be set ; :: thesis: ( b' in B' & a c= b' implies b c= b' )
assume that
A23: b' in B' and
A24: a c= b' ; :: thesis: b c= b'
consider b1', a' being Subset of X such that
A25: b' = b1' and
A26: a' ^|^ b1',G by A20, A23, Th33;
A27: [a',b'] in Maximal_wrt G by A25, A26, Def18;
consider a'', b'' being Subset of X such that
A28: [a'',b''] in Maximal_wrt G and
A29: [a'',b''] >= x' by Th28;
a'' c= a by A22, A29, Th15;
then a'' c= b' by A24, XBOOLE_1:1;
then A30: b'' c= b1' by A21, A25, A27, A28, Def21;
b c= b'' by A22, A29, Th15;
hence b c= b' by A25, A30, XBOOLE_1:1; :: thesis: verum

end;

hence x in X deps_encl_by B by A22; :: thesis: verum

end;

assume x in X deps_encl_by B ; :: thesis: x in G
then consider a, b being Subset of X such that
A31: x = [a,b] and
A32: for c being set st c in B & a c= c holds
b c= c ;
consider a', b' being Subset of X such that
A33: [a',b'] >= [a,a] and
A34: [a',b'] in Maximal_wrt G by A21, Def19;
A35: ( a' c= a & a c= b' ) by A33, Th15;
a' ^|^ b',G by A34, Def18;
then b' in B by A20;
then b c= b' by A32, A35;
then [a',b'] >= [a,b] by A35, Th15;
hence x in G by A31, A34, Def13; :: thesis: verum

end;

hence G = X deps_encl_by B by TARSKI:2; :: thesis: verum