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 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= b1 )
assume that
A8: c in BB9 and
A9: a c= c ; :: thesis: b c= b1
per cases ( K c= a or b c= a ) by A7;
suppose A10: K c= a ; :: thesis: b c= b1
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 { 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= b1
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