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

A1: field (Dependencies-Order X) = [:(bool X),(bool X):] by Th19;
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 Maximal_wrt F )
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();
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 A3: MA is finite Subset of by A1, XBOOLE_1:1;
[A,A] in F by Def16;
then MA <> {} by A2;
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 and
A7: B' in bool X and
A8: x = [A',B'] by ZFMISC_1:def 2;
reconsider A' = A', B' = B' as Subset of by A6, A7;
take A' ; :: thesis: ex B' being Subset of st
( [A',B'] >= [A,A] & [A',B'] in Maximal_wrt F )
take B' ; :: thesis: ( [A',B'] >= [A,A] & [A',B'] in Maximal_wrt F )
A9: ex y being Dependency of X st
( x = y & y >= [A,A] ) by A2, A5;
hence [A',B'] >= [A,A] by A8; :: 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 A10: z in F and
A11: z <> x and
A12: [x,z] in Dependencies-Order X ; :: thesis: contradiction
consider e, f being Dependency of X such that
A13: [x,z] = [e,f] and
A14: e <= f by A12;
x = e by A13, ZFMISC_1:33;
then A15: f >= [A,A] by A9, A14, Th14;
z = f by A13, ZFMISC_1:33;
then z in MA by A2, A10, A15;
hence contradiction by A4, A11, A12, WAYBEL_4:def 24; :: thesis: verum

end;

hence [A',B'] in Maximal_wrt F by A8, 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 ; :: 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 that
A16: [A,B] in Maximal_wrt F and
A17: [A',B'] in Maximal_wrt F and
A18: [A,B] >= [A',B'] ; :: thesis: ( A = A' & B = B' )
A19: [[A',B'],[A,B]] in Dependencies-Order X by A18;
assume ( not A = A' or not B = B' ) ; :: thesis: contradiction
then A20: [A,B] <> [A',B'] by ZFMISC_1:33;
[A',B'] is_maximal_wrt F, Dependencies-Order X by A17, Def1;
hence contradiction by A16, A20, A19, WAYBEL_4:def 24; :: thesis: verum

end;

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

proof

let A, B, A', B' be Subset of ; :: 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 that
A21: [A,B] in Maximal_wrt F and
A22: [A',B'] in Maximal_wrt F and
A23: A' c= B ; :: thesis: B' c= B
A24: A ^|^ B,F by A21, Def18;
[A',B'] >= [B,B'] by A23, Th15;
then [B,B'] in F by A22, Def13;
then A25: [A,B'] in F by A21, Th20;
B c= B \/ B' by XBOOLE_1:7;
then A26: [A,(B \/ B')] >= [A,B] by Th15;
A \/ A = A ;
then [A,(B \/ B')] in F by A21, A25, Def14;
then B \/ B' = B by A24, A26, Th29;
hence B' c= B by XBOOLE_1:11; :: thesis: verum

end;