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

proof

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

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

{X} c= bool X by ZFMISC_1:80;
hence x in bool X by A3; :: 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 BB' = {X} \/ { B where B is Subset of X : not K c= B } as non empty Subset-Family of X ;
A4: BB' is (B1) by Th41;
A5: BB' is (B2) by Th41;
set G = { [a,b] where a, b is Subset of X : for c being set st c in BB' & a c= c holds
b c= c } ;
A6: { [a,b] where a, b is Subset of X : for c being set st c in BB' & a c= c holds
b c= c } = X deps_encl_by BB' ;

now

let x be set ; :: thesis: ( ( x in F implies x in { [a,b] where a, b is Subset of X : for c being set st c in BB' & 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 BB' & 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 BB' & 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 BB' & a c= c holds
b c= c }
then consider a, b being Subset of X such that
A7: x = [a,b] and
A8: ( K c= a or b c= a ) by A1;

now

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

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

suppose A11: 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 A9, 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 A10, A11, XBOOLE_1:1; :: thesis: verum

end;

end;

end;

end;

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

hence b c= c by A10, XBOOLE_1:1; :: thesis: verum

end;

end;

end;

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

end;

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

now

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 BB' by XBOOLE_0:def 3;
hence b c= a by A13; :: thesis: verum

end;

hence x in F by A1, A12; :: thesis: verum

end;

then F = { [a,b] where a, b is Subset of X : for c being set st c in BB' & a c= c holds
b c= c } by TARSKI:2;
hence {X} \/ { B where B is Subset of X : not K c= B } = saturated-subsets F by A4, A5, A6, Th37; :: thesis: verum