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 b1 in {X} \/ { b2 where B is Subset of X : not K c= b2 } ) )
hereby :: thesis: ( x in saturated-subsets F implies b1 in {X} \/ { b2 where B is Subset of X : not K c= b2 } )
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 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: b1 in {X} \/ { b2 where B is Subset of X : not K c= b2 }
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: b1 in {X} \/ { b2 where B is Subset of X : not K c= b2 }
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: b1 in {X} \/ { b2 where B is Subset of X : not K c= b2 }
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