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 Th17;
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 Maximal_wrt F )
defpred S₁[ object ] means ex y being Dependency of X st
( $1 = y & y >= [A,A] );
consider MA being set such that
A2: for x being object holds
( x in MA iff ( x in F & S₁[x] ) ) from XBOOLE_0:sch 1();
MA c= F by A2;
then A3: MA is finite Subset of (field (Dependencies-Order X)) by A1, XBOOLE_1:1;
[A,A] in F by Def15;
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;
then x in F by A2;
then consider A9, B9 being object such that
A6: A9 in bool X and
A7: B9 in bool X and
A8: x = [A9,B9] by ZFMISC_1:def 2;
reconsider A9 = A9, B9 = B9 as Subset of X by A6, A7;
take A9 ; :: thesis: ex B9 being Subset of X st
( [A9,B9] >= [A,A] & [A9,B9] in Maximal_wrt F )
take B9 ; :: thesis: ( [A9,B9] >= [A,A] & [A9,B9] in Maximal_wrt F )
A9: ex y being Dependency of X st
( x = y & y >= [A,A] ) by A2, A5;
hence [A9,B9] >= [A,A] by A8; :: thesis: [A9,B9] 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 23 :: 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, XTUPLE_0:1;
then A15: f >= [A,A] by A9, A14, Th12;
z = f by A13, XTUPLE_0:1;
then z in MA by A2, A10, A15;
hence contradiction by A4, A11, A12; :: thesis: verum

end;

hence [A9,B9] 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, A9, B9 be Subset of X; :: according to ARMSTRNG:def 19 :: thesis: ( [A,B] in Maximal_wrt F & [A9,B9] in Maximal_wrt F & [A,B] >= [A9,B9] implies ( A = A9 & B = B9 ) )
assume that
A16: [A,B] in Maximal_wrt F and
A17: [A9,B9] in Maximal_wrt F and
A18: [A,B] >= [A9,B9] ; :: thesis: ( A = A9 & B = B9 )
A19: [[A9,B9],[A,B]] in Dependencies-Order X by A18;
assume ( not A = A9 or not B = B9 ) ; :: thesis: contradiction
then A20: [A,B] <> [A9,B9] by XTUPLE_0:1;
[A9,B9] is_maximal_wrt F, Dependencies-Order X by A17, Def1;
hence contradiction by A16, A20, A19; :: thesis: verum

end;

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

proof

let A, B, A9, B9 be Subset of X; :: according to ARMSTRNG:def 20 :: thesis: ( [A,B] in Maximal_wrt F & [A9,B9] in Maximal_wrt F & A9 c= B implies B9 c= B )
assume that
A21: [A,B] in Maximal_wrt F and
A22: [A9,B9] in Maximal_wrt F and
A23: A9 c= B ; :: thesis: B9 c= B
A24: A ^|^ B,F by A21;
[A9,B9] >= [B,B9] by A23;
then [B,B9] in F by A22, Def12;
then A25: [A,B9] in F by A21, Th18;
B c= B \/ B9 by XBOOLE_1:7;
then A26: [A,(B \/ B9)] >= [A,B] ;
A \/ A = A ;
then [A,(B \/ B9)] in F by A21, A25, Def13;
then B \/ B9 = B by A24, A26, Th27;
hence B9 c= B by XBOOLE_1:11; :: thesis: verum

end;