let X be non empty finite set ; :: thesis: for F being Full-family of X holds
( Maximal_wrt F is (M1) & Maximal_wrt F is (M2) & Maximal_wrt F is (M3) )
let F be full_family Dependency-set of X; :: thesis: ( Maximal_wrt F is (M1) & Maximal_wrt F is (M2) & Maximal_wrt F is (M3) )
set DOX = Dependencies-Order X;
set MEF = Maximal_wrt F;
thus Maximal_wrt F is (M1) :: thesis: ( Maximal_wrt F is (M2) & Maximal_wrt F is (M3) )

proof

let A be Subset of X; :: according to ARMSTRNG:def 19 :: thesis: ex A', B' being Subset of X st
( [A',B'] >= [A,A] & [A',B'] in Maximal_wrt F )
A1: field (Dependencies-Order X) = [:(bool X),(bool X):] by Th19;
defpred S₁[ set ] means ex y being Dependency of X st
( $1 = y & y >= [A,A] );
consider MA being set such that
A2: for x being set holds
( x in MA iff ( x in F & S₁[x] ) ) from XBOOLE_0:sch 1();
[A,A] in F by Def16;
then A3: MA <> {} by A2;
MA c= F

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in MA or x in F )
assume x in MA ; :: thesis: x in F
hence x in F by A2; :: thesis: verum

end;

then MA is finite Subset of (field (Dependencies-Order X)) by A1, XBOOLE_1:1;
then consider x being Element of MA such that
A4: x is_maximal_wrt MA, Dependencies-Order X by A3, Th2;
A5: x in MA by A4, WAYBEL_4:def 24;
then x in F by A2;
then consider A', B' being set such that
A6: ( A' in bool X & B' in bool X & x = [A',B'] ) by ZFMISC_1:def 2;
reconsider A' = A', B' = B' as Subset of X by A6;
take A' ; :: thesis: ex B' being Subset of X st
( [A',B'] >= [A,A] & [A',B'] in Maximal_wrt F )
take B' ; :: thesis: ( [A',B'] >= [A,A] & [A',B'] in Maximal_wrt F )
consider y being Dependency of X such that
A7: ( x = y & y >= [A,A] ) by A2, A5;
thus [A',B'] >= [A,A] by A6, A7; :: thesis: [A',B'] in Maximal_wrt F
x is_maximal_wrt F, Dependencies-Order X

proof

thus x in F by A2, A5; :: according to WAYBEL_4:def 24 :: thesis: for b₁ being set holds
( not b₁ in F or b₁ = x or not [x,b₁] in Dependencies-Order X )
given z being set such that A8: ( z in F & z <> x & [x,z] in Dependencies-Order X ) ; :: thesis: contradiction
consider e, f being Dependency of X such that
A9: ( [x,z] = [e,f] & e <= f ) by A8;
A10: ( x = e & z = f ) by A9, ZFMISC_1:33;
then f >= [A,A] by A7, A9, Th14;
then z in MA by A2, A8, A10;
hence contradiction by A4, A8, WAYBEL_4:def 24; :: thesis: verum

end;

hence [A',B'] in Maximal_wrt F by A6, Def1; :: thesis: verum

end;

thus Maximal_wrt F is (M2) :: thesis: Maximal_wrt F is (M3)

proof

let A, B, A', B' be Subset of X; :: according to ARMSTRNG:def 20 :: thesis: ( [A,B] in Maximal_wrt F & [A',B'] in Maximal_wrt F & [A,B] >= [A',B'] implies ( A = A' & B = B' ) )
assume A11: ( [A,B] in Maximal_wrt F & [A',B'] in Maximal_wrt F & [A,B] >= [A',B'] ) ; :: thesis: ( A = A' & B = B' )
A12: [A',B'] is_maximal_wrt F, Dependencies-Order X by A11, Def1;
assume ( not A = A' or not B = B' ) ; :: thesis: contradiction
then A13: [A,B] <> [A',B'] by ZFMISC_1:33;
[[A',B'],[A,B]] in Dependencies-Order X by A11;
hence contradiction by A11, A12, A13, WAYBEL_4:def 24; :: thesis: verum

end;

thus Maximal_wrt F is (M3) :: thesis: verum

proof

let A, B, A', B' be Subset of X; :: according to ARMSTRNG:def 21 :: thesis: ( [A,B] in Maximal_wrt F & [A',B'] in Maximal_wrt F & A' c= B implies B' c= B )
assume A14: ( [A,B] in Maximal_wrt F & [A',B'] in Maximal_wrt F & A' c= B ) ; :: thesis: B' c= B
then [A',B'] >= [B,B'] by Th15;
then A15: [B,B'] in F by A14, Def13;
A16: A \/ A = A ;
A17: A ^|^ B,F by A14, Def18;
[A,B'] in F by A14, A15, Th20;
then A18: [A,(B \/ B')] in F by A14, A16, Def14;
B c= B \/ B' by XBOOLE_1:7;
then [A,(B \/ B')] >= [A,B] by Th15;
then B \/ B' = B by A17, A18, Th29;
hence B' c= B by XBOOLE_1:11; :: thesis: verum

end;