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 ; :: 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 ; :: 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
A8: F is (F1) and
A9: F is (DC5) and
A10: F is (DC6) ; :: thesis: ( F is (F1) & F is (F2) & F is (F3) & F is (F4) )
thus F is (F1) by A8; :: thesis: ( F is (F2) & F is (F3) & F is (F4) )

A11: now

let A, B, C be Subset of ; :: thesis: ( [A,B] in F & [B,C] in F implies [A,C] in F )
assume that
A12: [A,B] in F and
A13: [B,C] in F ; :: thesis: [A,C] in F
[(B \/ A),C] in F by A10, A13, Def31;
then [(A \/ A),C] in F by A9, A12, 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 ; :: according to ARMSTRNG:def 13 :: thesis: ( [A,B] in F & [A,B] >= [A',B'] implies [A',B'] in F )
assume that
A14: [A,B] in F and
A15: [A,B] >= [A',B'] ; :: thesis: [A',B'] in F
A c= A' by A15, Th15;
then A' = A \/ (A' \ A) by XBOOLE_1:45;
then A16: [A',B] in F by A10, A14, Def31;
B' c= B by A15, Th15;
then A17: B = B' \/ (B \ B') by XBOOLE_1:45;
[B',B'] in F by A8, Def12;
then [B,B'] in F by A10, A17, Def31;
hence [A',B'] in F by A11, A16; :: thesis: verum

end;

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