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 )
assume A1: 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
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 } ;
A2: {[K,X]} \/ { [A,A] where A is Subset of X : not K c= A } = Maximal_wrt F by A1, Th32;
A3: [#] X = X ;
set ss = saturated-subsets F;

now

let x be set ; :: 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 A4: 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 A4, XBOOLE_0:def 3;

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

then A5: x = X by TARSKI:def 1;
[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 K ^|^ X,F by A2, Def18;
hence x in saturated-subsets F by A3, 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 A2, Def18;
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 Th33;
A10: [a,b] in {[K,X]} \/ { [A,A] where A is Subset of X : not K c= A } by A2, A9, Def18;

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 ZFMISC_1:33;
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: ( a = c & b = c ) by A11, ZFMISC_1:33;
c in { B where B is Subset of X : not K c= B } by A12;
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