let X be finite set ; :: thesis: for F being Dependency-set of X
for K being Subset of st F = { [A,B] where A, B is Subset of : ( K c= A or B c= A ) } holds
{[K,X]} \/ { [A,A] where A is Subset of : not K c= A } = Maximal_wrt F
let F be Dependency-set of X; :: thesis: for K being Subset of st F = { [A,B] where A, B is Subset of : ( K c= A or B c= A ) } holds
{[K,X]} \/ { [A,A] where A is Subset of : not K c= A } = Maximal_wrt F
let K be Subset of ; :: thesis: ( F = { [A,B] where A, B is Subset of : ( K c= A or B c= A ) } implies {[K,X]} \/ { [A,A] where A is Subset of : not K c= A } = Maximal_wrt F )
set M = {[K,X]} \/ { [A,A] where A is Subset of : not K c= A } ;
A1: {[K,X]} c= {[K,X]} \/ { [A,A] where A is Subset of : not K c= A } by XBOOLE_1:7;

A2: now

let A be Subset of ; :: thesis: ( not K c= A implies [A,A] in {[K,X]} \/ { [A,A] where A is Subset of : not K c= A } )
assume not K c= A ; :: thesis: [A,A] in {[K,X]} \/ { [A,A] where A is Subset of : not K c= A }
then A3: [A,A] in { [a,a] where a is Subset of : not K c= a } ;
{ [a,a] where a is Subset of : not K c= a } c= {[K,X]} \/ { [A,A] where A is Subset of : not K c= A } by XBOOLE_1:7;
hence [A,A] in {[K,X]} \/ { [A,A] where A is Subset of : not K c= A } by A3; :: thesis: verum

end;

A4: [#] X = X ;
A5: {[K,X]} \/ { [A,A] where A is Subset of : not K c= A } c= [:(bool X),(bool X):]

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {[K,X]} \/ { [A,A] where A is Subset of : not K c= A } or x in [:(bool X),(bool X):] )
assume A6: x in {[K,X]} \/ { [A,A] where A is Subset of : not K c= A } ; :: thesis: x in [:(bool X),(bool X):]

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

suppose x in {[K,X]} ; :: thesis: x in [:(bool X),(bool X):]

then x = [K,X] by TARSKI:def 1;
hence x in [:(bool X),(bool X):] by A4, ZFMISC_1:def 2; :: thesis: verum

end;

suppose x in { [A,A] where A is Subset of : not K c= A } ; :: thesis: x in [:(bool X),(bool X):]

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

end;

end;

end;

A7: now

let A, B be Subset of ; :: thesis: ( not [A,B] in {[K,X]} \/ { [A,A] where A is Subset of : not K c= A } or [b₁,b₂] = [K,X] or ( not K c= b₁ & b₁ = b₂ ) )
assume A8: [A,B] in {[K,X]} \/ { [A,A] where A is Subset of : not K c= A } ; :: thesis: ( [b₁,b₂] = [K,X] or ( not K c= b₁ & b₁ = b₂ ) )

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

suppose [A,B] in {[K,X]} ; :: thesis: ( [b₁,b₂] = [K,X] or ( not K c= b₁ & b₁ = b₂ ) )

hence ( [A,B] = [K,X] or ( not K c= A & A = B ) ) by TARSKI:def 1; :: thesis: verum

end;

suppose [A,B] in { [a,a] where a is Subset of : not K c= a } ; :: thesis: ( [b₁,b₂] = [K,X] or ( not K c= b₁ & b₁ = b₂ ) )

then consider a being Subset of such that
A9: [A,B] = [a,a] and
A10: not K c= a ;
A = a by A9, ZFMISC_1:33;
hence ( [A,B] = [K,X] or ( not K c= A & A = B ) ) by A9, A10, ZFMISC_1:33; :: thesis: verum

end;

end;

end;

reconsider M = {[K,X]} \/ { [A,A] where A is Subset of : not K c= A } as Dependency-set of X by A5;
set FF = { [A,B] where A, B is Subset of : ex A', B' being Subset of st
( [A',B'] >= [A,B] & [A',B'] in M ) } ;
A11: { [A,B] where A, B is Subset of : ex A', B' being Subset of st
( [A',B'] >= [A,B] & [A',B'] in M ) } c= [:(bool X),(bool X):]

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { [A,B] where A, B is Subset of : ex A', B' being Subset of st
( [A',B'] >= [A,B] & [A',B'] in M ) } or x in [:(bool X),(bool X):] )
assume x in { [A,B] where A, B is Subset of : ex A', B' being Subset of st
( [A',B'] >= [A,B] & [A',B'] in M ) } ; :: thesis: x in [:(bool X),(bool X):]
then ex A, B being Subset of st
( x = [A,B] & ex A', B' being Subset of st
( [A',B'] >= [A,B] & [A',B'] in M ) ) ;
hence x in [:(bool X),(bool X):] ; :: thesis: verum

end;

A12: M is (M2)

proof

let A, B, A', B' be Subset of ; :: according to ARMSTRNG:def 20 :: thesis: ( [A,B] in M & [A',B'] in M & [A,B] >= [A',B'] implies ( A = A' & B = B' ) )
assume that
A13: [A,B] in M and
A14: [A',B'] in M and
A15: [A,B] >= [A',B'] ; :: thesis: ( A = A' & B = B' )
A16: A c= A' by A15, Th15;
A17: B' c= B by A15, Th15;

per cases ( [A,B] = [K,X] or ( not K c= A & A = B ) ) by A7, A13;

suppose A18: [A,B] = [K,X] ; :: thesis: ( A = A' & B = B' )

thus ( A = A' & B = B' ) :: thesis: verum

proof

per cases ( [A',B'] = [K,X] or ( not K c= A' & A' = B' ) ) by A7, A14;

suppose [A',B'] = [K,X] ; :: thesis: ( A = A' & B = B' )

hence ( A = A' & B = B' ) by A18, ZFMISC_1:33; :: thesis: verum

end;

suppose ( not K c= A' & A' = B' ) ; :: thesis: ( A = A' & B = B' )

hence ( A = A' & B = B' ) by A16, A18, ZFMISC_1:33; :: thesis: verum

end;

end;

end;

end;

suppose A19: ( not K c= A & A = B ) ; :: thesis: ( A = A' & B = B' )

thus ( A = A' & B = B' ) :: thesis: verum

proof

per cases ( [A',B'] = [K,X] or ( not K c= A' & A' = B' ) ) by A7, A14;

suppose [A',B'] = [K,X] ; :: thesis: ( A = A' & B = B' )

then B' = X by ZFMISC_1:33;
then B = X by A17, XBOOLE_0:def 10;
hence ( A = A' & B = B' ) by A19; :: thesis: verum

end;

suppose ( not K c= A' & A' = B' ) ; :: thesis: ( A = A' & B = B' )

hence ( A = A' & B = B' ) by A16, A17, A19, XBOOLE_0:def 10; :: thesis: verum

end;

end;

end;

end;

end;

end;

reconsider FF = { [A,B] where A, B is Subset of : ex A', B' being Subset of st
( [A',B'] >= [A,B] & [A',B'] in M ) } as Dependency-set of X by A11;
assume A20: F = { [A,B] where A, B is Subset of : ( K c= A or B c= A ) } ; :: thesis: {[K,X]} \/ { [A,A] where A is Subset of : not K c= A } = Maximal_wrt F

A21: now

let x be set ; :: thesis: ( ( x in F implies x in FF ) & ( x in FF implies b₁ in F ) )

hereby :: thesis: ( x in FF implies b₁ in F )

A22: { [a,a] where a is Subset of : not K c= a } c= M by XBOOLE_1:7;
A23: [K,X] in {[K,X]} by TARSKI:def 1;
A24: {[K,X]} c= M by XBOOLE_1:7;
assume x in F ; :: thesis: x in FF
then consider A, B being Subset of such that
A25: x = [A,B] and
A26: ( K c= A or B c= A ) by A20;

per cases ( K c= A or not K c= A ) ;

suppose K c= A ; :: thesis: x in FF

then [K,([#] X)] >= [A,B] by Th15;
hence x in FF by A25, A24, A23; :: thesis: verum

end;

suppose A27: not K c= A ; :: thesis: x in FF

then A28: [A,A] in { [a,a] where a is Subset of : not K c= a } ;
[A,A] >= [A,B] by A26, A27, Th15;
hence x in FF by A25, A22, A28; :: thesis: verum

end;

end;

end;

assume x in FF ; :: thesis: b₁ in F
then consider A, B being Subset of such that
A29: x = [A,B] and
A30: ex A', B' being Subset of st
( [A',B'] >= [A,B] & [A',B'] in M ) ;
consider A', B' being Subset of such that
A31: [A',B'] >= [A,B] and
A32: [A',B'] in M by A30;

per cases ( [A',B'] in {[K,X]} or [A',B'] in { [a,a] where a is Subset of : not K c= a } ) by A32, XBOOLE_0:def 3;

suppose [A',B'] in {[K,X]} ; :: thesis: b₁ in F

then [A',B'] = [K,X] by TARSKI:def 1;
then A' = K by ZFMISC_1:33;
then K c= A by A31, Th15;
hence x in F by A20, A29; :: thesis: verum

end;

suppose [A',B'] in { [a,a] where a is Subset of : not K c= a } ; :: thesis: b₁ in F

then consider a being Subset of such that
A33: [A',B'] = [a,a] and
not K c= a ;
A34: A' = a by A33, ZFMISC_1:33;
A35: B' = a by A33, ZFMISC_1:33;
A36: B c= B' by A31, Th15;
A' c= A by A31, Th15;
then B c= A by A34, A35, A36, XBOOLE_1:1;
hence x in F by A20, A29; :: thesis: verum

end;

end;

end;

A37: M is (M3)

proof

let A, B, A', B' be Subset of ; :: according to ARMSTRNG:def 21 :: thesis: ( [A,B] in M & [A',B'] in M & A' c= B implies B' c= B )
assume that
A38: [A,B] in M and
A39: [A',B'] in M and
A40: A' c= B ; :: thesis: B' c= B

per cases ( [A,B] = [K,X] or ( not K c= A & A = B ) ) by A7, A38;

suppose [A,B] = [K,X] ; :: thesis: B' c= B

then B = X by ZFMISC_1:33;
hence B' c= B ; :: thesis: verum

end;

suppose A41: ( not K c= A & A = B ) ; :: thesis: B' c= B

thus B' c= B :: thesis: verum

proof

per cases ( [A',B'] = [K,X] or ( not K c= A' & A' = B' ) ) by A7, A39;

suppose [A',B'] = [K,X] ; :: thesis: B' c= B

hence B' c= B by A40, A41, ZFMISC_1:33; :: thesis: verum

end;

suppose ( not K c= A' & A' = B' ) ; :: thesis: B' c= B

hence B' c= B by A40; :: thesis: verum

end;

end;

end;

end;

end;

end;

A42: [K,X] in {[K,X]} by TARSKI:def 1;
M is (M1)

proof

let A be Subset of ; :: according to ARMSTRNG:def 19 :: thesis: ex A', B' being Subset of st
( [A',B'] >= [A,A] & [A',B'] in M )

per cases ( K c= A or not K c= A ) ;

suppose A43: K c= A ; :: thesis: ex A', B' being Subset of st
( [A',B'] >= [A,A] & [A',B'] in M )

take A' = K; :: thesis: ex B' being Subset of st
( [A',B'] >= [A,A] & [A',B'] in M )
take B' = [#] X; :: thesis: ( [A',B'] >= [A,A] & [A',B'] in M )
thus [A',B'] >= [A,A] by A43, Th15; :: thesis: [A',B'] in M
thus [A',B'] in M by A42, A1; :: thesis: verum

end;

suppose A44: not K c= A ; :: thesis: ex A', B' being Subset of st
( [A',B'] >= [A,A] & [A',B'] in M )

take A' = A; :: thesis: ex B' being Subset of st
( [A',B'] >= [A,A] & [A',B'] in M )
take B' = A; :: thesis: ( [A',B'] >= [A,A] & [A',B'] in M )
thus [A',B'] >= [A,A] ; :: thesis: [A',B'] in M
thus [A',B'] in M by A2, A44; :: thesis: verum

end;

end;

end;

then M = Maximal_wrt FF by A12, A37, Th31;
hence {[K,X]} \/ { [A,A] where A is Subset of : not K c= A } = Maximal_wrt F by A21, TARSKI:2; :: thesis: verum