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 ) ) )
set F = X deps_encl_by B;
reconsider F9 = X deps_encl_by B as Full-family of X by Th33;
set ss = saturated-subsets (X deps_encl_by B);
set M = Maximal_wrt F9;
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 B9 = B as non empty set ;
A2: X in B by A1;
now :: thesis: for x being object holds
( ( 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 ) )
let x be object ; :: 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 Th34;
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 Th31;
[a,b] in Maximal_wrt F9 by A4;
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: b = bb by A5, XTUPLE_0:1;
set S = { b9 where b9 is Element of B9 : a c= b9 } ;
A8: { b9 where b9 is Element of B9 : a c= b9 } c= bool X
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { b9 where b9 is Element of B9 : a c= b9 } or x in bool X )
assume x in { b9 where b9 is Element of B9 : a c= b9 } ; :: thesis: x in bool X
then consider b9 being Element of B9 such that
A9: x = b9 and
a c= b9 ;
b9 in B9 ;
hence x in bool X by A9; :: thesis: verum
end;
A10: { b9 where b9 is Element of B9 : a c= b9 } c= B
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { b9 where b9 is Element of B9 : a c= b9 } or x in B )
assume x in { b9 where b9 is Element of B9 : a c= b9 } ; :: thesis: x in B
then ex b9 being Element of B9 st
( x = b9 & a c= b9 ) ;
hence x in B ; :: thesis: verum
end;
A11: X in { b9 where b9 is Element of B9 : a c= b9 } by A2;
reconsider S = { b9 where b9 is Element of B9 : a c= b9 } as Subset-Family of X by A8;
set mS = Intersect S;
reconsider mS = Intersect S as Subset of X ;
A12: a = aa by A5, XTUPLE_0:1;
A13: b c= mS
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in b or x in mS )
assume A14: x in b ; :: thesis: x in mS
now :: thesis: for Y being set st Y in S holds
x in Y
let Y be set ; :: thesis: ( Y in S implies x in Y )
assume Y in S ; :: thesis: x in Y
then consider b9 being Element of B9 such that
A15: Y = b9 and
A16: a c= b9 ;
b c= b9 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 9; :: thesis: verum
end;
now :: thesis: not b <> mS
now :: thesis: for c being set st c in B & a c= c holds
mS c= c
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:3;
hence mS c= c by A11, SETFAM_1:def 9; :: 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;
hence contradiction by A4, A20, A19, Th27; :: thesis: verum
end;
hence x in B by A1, 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 Th28;
now :: thesis: for x being object holds
( ( x in G implies x in X deps_encl_by B ) & ( x in X deps_encl_by B implies x in G ) )
let x be object ; :: 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 x9 = x1 as Dependency of X ;
consider a, b being Subset of X such that
A23: x9 = [a,b] by Th8;
now :: thesis: for b9 being set st b9 in B9 & a c= b9 holds
b c= b9
consider a99, b99 being Subset of X such that
A24: [a99,b99] in Maximal_wrt G and
A25: [a99,b99] >= x9 by Th26;
A26: b c= b99 by A23, A25;
let b9 be set ; :: thesis: ( b9 in B9 & a c= b9 implies b c= b9 )
assume that
A27: b9 in B9 and
A28: a c= b9 ; :: thesis: b c= b9
consider b19, a9 being Subset of X such that
A29: b9 = b19 and
A30: a9 ^|^ b19,G by A21, A27, Th31;
a99 c= a by A23, A25;
then A31: a99 c= b9 by A28;
[a9,b9] in Maximal_wrt G by A29, A30;
then b99 c= b19 by A22, A29, A24, A31;
hence b c= b9 by A29, A26; :: 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 X such that
A32: x = [a,b] and
A33: for c being set st c in B & a c= c holds
b c= c ;
consider a9, b9 being Subset of X such that
A34: [a9,b9] >= [a,a] and
A35: [a9,b9] in Maximal_wrt G by A22;
A36: a9 c= a by A34;
a9 ^|^ b9,G by A35;
then A37: b9 in B by A21;
a c= b9 by A34;
then b c= b9 by A33, A37;
then [a9,b9] >= [a,b] by A36;
hence x in G by A32, A35, Def12; :: thesis: verum
end;
hence G = X deps_encl_by B by TARSKI:2; :: thesis: verum