let X be non empty 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 } ;
{X} \/ { B where B is Subset of X : not K c= B } c= bool X

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {X} \/ { B where B is Subset of X : not K c= B } or x in bool X )
assume A1: x in {X} \/ { B where B is Subset of X : not K c= B } ; :: thesis: x in bool X

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

suppose A2: x in {X} ; :: thesis: x in bool X

{X} c= bool X by ZFMISC_1:68;
hence x in bool X by A2; :: thesis: verum

end;

suppose x in { B where B is Subset of X : not K c= B } ; :: thesis: x in bool X

then ex B being Subset of X st
( x = B & not K c= B ) ;
hence x in bool X ; :: thesis: verum

end;

end;

end;

then reconsider BB9 = {X} \/ { B where B is Subset of X : not K c= B } as non empty Subset-Family of X ;
set G = { [a,b] where a, b is Subset of X : for c being set st c in BB9 & a c= c holds
b c= c } ;
A3: { [a,b] where a, b is Subset of X : for c being set st c in BB9 & a c= c holds
b c= c } = X deps_encl_by BB9 ;
A4: BB9 is (B2) by Th39;
assume A5: 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

now :: thesis: for x being object holds
( ( x in F implies x in { [a,b] where a, b is Subset of X : for c being set st c in BB9 & a c= c holds
b c= c } ) & ( x in { [a,b] where a, b is Subset of X : for c being set st c in BB9 & a c= c holds
b c= c } implies x in F ) )

let x be object ; :: thesis: ( ( x in F implies x in { [a,b] where a, b is Subset of X : for c being set st c in BB9 & a c= c holds
b c= c } ) & ( x in { [a,b] where a, b is Subset of X : for c being set st c in BB9 & a c= c holds
b c= c } implies x in F ) )

hereby :: thesis: ( x in { [a,b] where a, b is Subset of X : for c being set st c in BB9 & a c= c holds
b c= c } implies x in F )

assume x in F ; :: thesis: x in { [a,b] where a, b is Subset of X : for c being set st c in BB9 & a c= c holds
b c= c }
then consider a, b being Subset of X such that
A6: x = [a,b] and
A7: ( K c= a or b c= a ) by A5;

now :: thesis: for c being set st c in BB9 & a c= c holds
b c= c

let c be set ; :: thesis: ( c in BB9 & a c= c implies b c= b₁ )
assume that
A8: c in BB9 and
A9: a c= c ; :: thesis: b c= b₁

per cases ( K c= a or b c= a ) by A7;

suppose A10: K c= a ; :: thesis: b c= b₁

thus b c= c :: thesis: verum

proof

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

suppose c in {X} ; :: thesis: b c= c

then c = X by TARSKI:def 1;
hence b c= c ; :: thesis: verum

end;

suppose c in { B where B is Subset of X : not K c= B } ; :: thesis: b c= c

then ex B being Subset of X st
( c = B & not K c= B ) ;
hence b c= c by A9, A10; :: thesis: verum

end;

end;

end;

end;

suppose b c= a ; :: thesis: b c= b₁

hence b c= c by A9; :: thesis: verum

end;

end;

end;

hence x in { [a,b] where a, b is Subset of X : for c being set st c in BB9 & a c= c holds
b c= c } by A6; :: thesis: verum

end;

assume x in { [a,b] where a, b is Subset of X : for c being set st c in BB9 & a c= c holds
b c= c } ; :: thesis: x in F
then consider a, b being Subset of X such that
A11: x = [a,b] and
A12: for c being set st c in BB9 & a c= c holds
b c= c ;

now :: thesis: ( not K c= a implies b c= a )

assume not K c= a ; :: thesis: b c= a
then a in { B where B is Subset of X : not K c= B } ;
then a in BB9 by XBOOLE_0:def 3;
hence b c= a by A12; :: thesis: verum

end;

hence x in F by A5, A11; :: thesis: verum

end;

then A13: F = { [a,b] where a, b is Subset of X : for c being set st c in BB9 & a c= c holds
b c= c } by TARSKI:2;
BB9 is (B1) by Th39;
hence {X} \/ { B where B is Subset of X : not K c= B } = saturated-subsets F by A4, A3, A13, Th35; :: thesis: verum