let X be set ; :: thesis: for F being Dependency-set of X holds
( F is (F1) & F is (F2) & F is (F3) & F is (F4) iff ( F is (F1) & F is (DC5) & F is (DC6) ) )
let F be Dependency-set of X; :: thesis: ( F is (F1) & F is (F2) & F is (F3) & F is (F4) iff ( F is (F1) & F is (DC5) & F is (DC6) ) )

hereby :: thesis: ( F is (F1) & F is (DC5) & F is (DC6) implies ( F is (F1) & F is (F2) & F is (F3) & F is (F4) ) )

assume that
A1: F is (F1) and
A2: F is (F2) and
A3: F is (F3) and
A4: F is (F4) ; :: thesis: ( F is (F1) & F is (DC5) & F is (DC6) )
thus F is (F1) by A1; :: thesis: ( F is (DC5) & F is (DC6) )
thus F is (DC5) :: thesis: F is (DC6)

proof

let A, B, C, D be Subset of X; :: according to ARMSTRNG:def 30 :: thesis: ( [A,B] in F & [(B \/ C),D] in F implies [(A \/ C),D] in F )
assume that
A5: [A,B] in F and
A6: [(B \/ C),D] in F ; :: thesis: [(A \/ C),D] in F
[C,C] in F by A1, Def12;
then [(A \/ C),(B \/ C)] in F by A4, A5, Def14;
hence [(A \/ C),D] in F by A2, A6, Th20; :: thesis: verum

end;

thus F is (DC6) :: thesis: verum

proof

let A, B, C be Subset of X; :: according to ARMSTRNG:def 31 :: thesis: ( [A,B] in F implies [(A \/ C),B] in F )
assume A7: [A,B] in F ; :: thesis: [(A \/ C),B] in F
A c= A \/ C by XBOOLE_1:7;
then [(A \/ C),A] in F by A1, A3, Def16;
hence [(A \/ C),B] in F by A2, A7, Th20; :: thesis: verum

end;

end;

assume that
A9: F is (F1) and
A10: F is (DC5) and
A11: F is (DC6) ; :: thesis: ( F is (F1) & F is (F2) & F is (F3) & F is (F4) )
thus F is (F1) by A9; :: thesis: ( F is (F2) & F is (F3) & F is (F4) )

A12: now

let A, B, C be Subset of X; :: thesis: ( [A,B] in F & [B,C] in F implies [A,C] in F )
assume that
A13: [A,B] in F and
A14: [B,C] in F ; :: thesis: [A,C] in F
[(B \/ A),C] in F by A11, A14, Def31;
then [(A \/ A),C] in F by A10, A13, Def30;
hence [A,C] in F ; :: thesis: verum

end;

hence F is (F2) by Th20; :: thesis: ( F is (F3) & F is (F4) )
thus F is (F3) :: thesis: F is (F4)

proof

let A, B, A', B' be Subset of X; :: according to ARMSTRNG:def 13 :: thesis: ( [A,B] in F & [A,B] >= [A',B'] implies [A',B'] in F )
assume that
A15: [A,B] in F and
A16: [A,B] >= [A',B'] ; :: thesis: [A',B'] in F
A17: ( A c= A' & B' c= B ) by A16, Th15;
then A' = A \/ (A' \ A) by XBOOLE_1:45;
then A18: [A',B] in F by A11, A15, Def31;
A19: [B',B'] in F by A9, Def12;
B = B' \/ (B \ B') by A17, XBOOLE_1:45;
then [B,B'] in F by A11, A19, Def31;
hence [A',B'] in F by A12, A18; :: thesis: verum

end;

let A, B, A', B' be Subset of X; :: according to ARMSTRNG:def 14 :: thesis: ( [A,B] in F & [A',B'] in F implies [(A \/ A'),(B \/ B')] in F )
assume that
A20: [A,B] in F and
A21: [A',B'] in F ; :: thesis: [(A \/ A'),(B \/ B')] in F
[(B \/ B'),(B \/ B')] in F by A9, Def12;
then [(A \/ B'),(B \/ B')] in F by A10, A20, Def30;
hence [(A \/ A'),(B \/ B')] in F by A10, A21, Def30; :: thesis: verum