let X be finite set ; :: thesis: for F being Dependency-set of X
for K being Subset of X st F = { [A,B] where A, B is Subset of X : ( K c= A or B c= A ) } holds
{X} \/ { B where B is Subset of X : not K c= B } = saturated-subsets F
let F be Dependency-set of X; :: thesis: for K being Subset of X st F = { [A,B] where A, B is Subset of X : ( K c= A or B c= A ) } holds
{X} \/ { B where B is Subset of X : not K c= B } = saturated-subsets F
let K be Subset of X; :: thesis: ( F = { [A,B] where A, B is Subset of X : ( K c= A or B c= A ) } implies {X} \/ { B where B is Subset of X : not K c= B } = saturated-subsets F )
set BB = {X} \/ { B where B is Subset of X : not K c= B } ;
set M = {[K,X]} \/ { [A,A] where A is Subset of X : not K c= A } ;
set ss = saturated-subsets F;
assume F = { [A,B] where A, B is Subset of X : ( K c= A or B c= A ) } ; :: thesis: {X} \/ { B where B is Subset of X : not K c= B } = saturated-subsets F
then A1: {[K,X]} \/ { [A,A] where A is Subset of X : not K c= A } = Maximal_wrt F by Th30;
A2: [#] X = X ;

now :: thesis: for x being object holds
( ( x in {X} \/ { B where B is Subset of X : not K c= B } implies x in saturated-subsets F ) & ( x in saturated-subsets F implies x in {X} \/ { B where B is Subset of X : not K c= B } ) )

let x be object ; :: thesis: ( ( x in {X} \/ { B where B is Subset of X : not K c= B } implies x in saturated-subsets F ) & ( x in saturated-subsets F implies b₁ in {X} \/ { b₂ where B is Subset of X : not K c= b₂ } ) )

hereby :: thesis: ( x in saturated-subsets F implies b₁ in {X} \/ { b₂ where B is Subset of X : not K c= b₂ } )

assume A3: x in {X} \/ { B where B is Subset of X : not K c= B } ; :: thesis: x in saturated-subsets F

per cases ( x in {X} or x in { B where B is Subset of X : not K c= B } ) by A3, XBOOLE_0:def 3;

suppose A4: x in {X} ; :: thesis: x in saturated-subsets F

[K,X] in {[K,X]} by TARSKI:def 1;
then [K,X] in {[K,X]} \/ { [A,A] where A is Subset of X : not K c= A } by XBOOLE_0:def 3;
then A5: K ^|^ X,F by A1;
x = X by A4, TARSKI:def 1;
hence x in saturated-subsets F by A2, A5; :: thesis: verum

end;

suppose x in { B where B is Subset of X : not K c= B } ; :: thesis: x in saturated-subsets F

then consider B being Subset of X such that
A6: x = B and
A7: not K c= B ;
[B,B] in { [A,A] where A is Subset of X : not K c= A } by A7;
then [B,B] in {[K,X]} \/ { [A,A] where A is Subset of X : not K c= A } by XBOOLE_0:def 3;
then B ^|^ B,F by A1;
hence x in saturated-subsets F by A6; :: thesis: verum

end;

end;

end;

assume x in saturated-subsets F ; :: thesis: b₁ in {X} \/ { b₂ where B is Subset of X : not K c= b₂ }
then consider b, a being Subset of X such that
A8: x = b and
A9: a ^|^ b,F by Th31;
A10: [a,b] in {[K,X]} \/ { [A,A] where A is Subset of X : not K c= A } by A1, A9;

per cases ( [a,b] in {[K,X]} or [a,b] in { [A,A] where A is Subset of X : not K c= A } ) by A10, XBOOLE_0:def 3;

suppose [a,b] in {[K,X]} ; :: thesis: b₁ in {X} \/ { b₂ where B is Subset of X : not K c= b₂ }

then [a,b] = [K,X] by TARSKI:def 1;
then b = X by XTUPLE_0:1;
then b in {X} by TARSKI:def 1;
hence x in {X} \/ { B where B is Subset of X : not K c= B } by A8, XBOOLE_0:def 3; :: thesis: verum

end;

suppose [a,b] in { [A,A] where A is Subset of X : not K c= A } ; :: thesis: b₁ in {X} \/ { b₂ where B is Subset of X : not K c= b₂ }

then consider c being Subset of X such that
A11: [a,b] = [c,c] and
A12: not K c= c ;
A13: c in { B where B is Subset of X : not K c= B } by A12;
b = c by A11, XTUPLE_0:1;
hence x in {X} \/ { B where B is Subset of X : not K c= B } by A8, A13, XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence {X} \/ { B where B is Subset of X : not K c= B } = saturated-subsets F by TARSKI:2; :: thesis: verum