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
{[K,X]} \/ { [A,A] where A is Subset of X : not K c= A } = Maximal_wrt 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
{[K,X]} \/ { [A,A] where A is Subset of X : not K c= A } = Maximal_wrt 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 {[K,X]} \/ { [A,A] where A is Subset of X : not K c= A } = Maximal_wrt F )
set M = {[K,X]} \/ { [A,A] where A is Subset of X : not K c= A } ;
A1: {[K,X]} c= {[K,X]} \/ { [A,A] where A is Subset of X : not K c= A } by XBOOLE_1:7;

A2: now

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

end;

A4: [#] X = X ;
A5: {[K,X]} \/ { [A,A] where A is Subset of X : 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 X : not K c= A } or x in [:(bool X),(bool X):] )
assume A6: x in {[K,X]} \/ { [A,A] where A is Subset of X : 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 X : 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 X : not K c= A } ; :: thesis: x in [:(bool X),(bool X):]

then ex A being Subset of X 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 X; :: thesis: ( not [A,B] in {[K,X]} \/ { [A,A] where A is Subset of X : 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 X : 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 X : 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 X : not K c= a } ; :: thesis: ( [b₁,b₂] = [K,X] or ( not K c= b₁ & b₁ = b₂ ) )

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

end;

end;

end;

reconsider M = {[K,X]} \/ { [A,A] where A is Subset of X : not K c= A } as Dependency-set of X by A5;
set FF = { [A,B] where A, B is Subset of X : ex A9, B9 being Subset of X st
( [A9,B9] >= [A,B] & [A9,B9] in M ) } ;
A11: { [A,B] where A, B is Subset of X : ex A9, B9 being Subset of X st
( [A9,B9] >= [A,B] & [A9,B9] 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 X : ex A9, B9 being Subset of X st
( [A9,B9] >= [A,B] & [A9,B9] in M ) } or x in [:(bool X),(bool X):] )
assume x in { [A,B] where A, B is Subset of X : ex A9, B9 being Subset of X st
( [A9,B9] >= [A,B] & [A9,B9] in M ) } ; :: thesis: x in [:(bool X),(bool X):]
then ex A, B being Subset of X st
( x = [A,B] & ex A9, B9 being Subset of X st
( [A9,B9] >= [A,B] & [A9,B9] in M ) ) ;
hence x in [:(bool X),(bool X):] ; :: thesis: verum

end;

A12: M is (M2)

proof

let A, B, A9, B9 be Subset of X; :: according to ARMSTRNG:def 19 :: thesis: ( [A,B] in M & [A9,B9] in M & [A,B] >= [A9,B9] implies ( A = A9 & B = B9 ) )
assume that
A13: [A,B] in M and
A14: [A9,B9] in M and
A15: [A,B] >= [A9,B9] ; :: thesis: ( A = A9 & B = B9 )
A16: A c= A9 by A15, Th15;
A17: B9 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 = A9 & B = B9 )

thus ( A = A9 & B = B9 ) :: thesis: verum

proof

per cases ( [A9,B9] = [K,X] or ( not K c= A9 & A9 = B9 ) ) by A7, A14;

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

hence ( A = A9 & B = B9 ) by A18, ZFMISC_1:27; :: thesis: verum

end;

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

hence ( A = A9 & B = B9 ) by A16, A18, ZFMISC_1:27; :: thesis: verum

end;

end;

end;

end;

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

thus ( A = A9 & B = B9 ) :: thesis: verum

proof

per cases ( [A9,B9] = [K,X] or ( not K c= A9 & A9 = B9 ) ) by A7, A14;

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

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

end;

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

hence ( A = A9 & B = B9 ) 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 X : ex A9, B9 being Subset of X st
( [A9,B9] >= [A,B] & [A9,B9] in M ) } as Dependency-set of X by A11;
assume A20: F = { [A,B] where A, B is Subset of X : ( K c= A or B c= A ) } ; :: thesis: {[K,X]} \/ { [A,A] where A is Subset of X : 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 X : 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 X 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 X : 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 X such that
A29: x = [A,B] and
A30: ex A9, B9 being Subset of X st
( [A9,B9] >= [A,B] & [A9,B9] in M ) ;
consider A9, B9 being Subset of X such that
A31: [A9,B9] >= [A,B] and
A32: [A9,B9] in M by A30;

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

suppose [A9,B9] in {[K,X]} ; :: thesis: b₁ in F

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

end;

suppose [A9,B9] in { [a,a] where a is Subset of X : not K c= a } ; :: thesis: b₁ in F

then consider a being Subset of X such that
A33: [A9,B9] = [a,a] and
not K c= a ;
A34: A9 = a by A33, ZFMISC_1:27;
A35: B9 = a by A33, ZFMISC_1:27;
A36: B c= B9 by A31, Th15;
A9 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, A9, B9 be Subset of X; :: according to ARMSTRNG:def 20 :: thesis: ( [A,B] in M & [A9,B9] in M & A9 c= B implies B9 c= B )
assume that
A38: [A,B] in M and
A39: [A9,B9] in M and
A40: A9 c= B ; :: thesis: B9 c= B

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

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

then B = X by ZFMISC_1:27;
hence B9 c= B ; :: thesis: verum

end;

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

thus B9 c= B :: thesis: verum

proof

per cases ( [A9,B9] = [K,X] or ( not K c= A9 & A9 = B9 ) ) by A7, A39;

suppose [A9,B9] = [K,X] ; :: thesis: B9 c= B

hence B9 c= B by A40, A41, ZFMISC_1:27; :: thesis: verum

end;

suppose ( not K c= A9 & A9 = B9 ) ; :: thesis: B9 c= B

hence B9 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 X; :: according to ARMSTRNG:def 18 :: thesis: ex A9, B9 being Subset of X st
( [A9,B9] >= [A,A] & [A9,B9] in M )

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

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

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

end;

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

take A9 = A; :: thesis: ex B9 being Subset of X st
( [A9,B9] >= [A,A] & [A9,B9] in M )
take B9 = A; :: thesis: ( [A9,B9] >= [A,A] & [A9,B9] in M )
thus [A9,B9] >= [A,A] ; :: thesis: [A9,B9] in M
thus [A9,B9] 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 X : not K c= A } = Maximal_wrt F by A21, TARSKI:1; :: thesis: verum