let X be non empty finite set ; :: thesis: for B being Subset-Family of 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 ; :: 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 ) ) )
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';
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 ) )
then reconsider B' = B as non empty set by Def4;
A2: X in B 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 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 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: b = bb by A5, ZFMISC_1:33;
set S = { b' where b' is Element of B' : a c= b' } ;
A8: { 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
A9: x = b' and
a c= b' ;
b' in B' ;
hence x in bool X by A9; :: thesis: verum

end;

A10: { 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 ex b' being Element of B' st
( x = b' & a c= b' ) ;
hence x in B ; :: thesis: verum

end;

A11: X in { b' where b' is Element of B' : a c= b' } by A2;
reconsider S = { b' where b' is Element of B' : a c= b' } as Subset-Family of by A8;
set mS = Intersect S;
reconsider mS = Intersect S as Subset of ;
A12: a = aa by A5, ZFMISC_1:33;
A13: b c= mS

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in b or x in mS )
assume A14: 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
A15: Y = b' and
A16: a c= b' ;
b c= b' by A6, A12, A7, A16;
hence x in Y by A14, A15; :: thesis: verum

end;

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

end;

now

now

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

end;

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

end;

hence x in B by A1, A2, A3, A10, 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 A21: B = saturated-subsets G ; :: thesis: G = X deps_encl_by B
set MG = Maximal_wrt G;
A22: ( 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 such that
A23: x' = [a,b] by Th9;

now

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

end;

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

end;

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

end;

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