let X be set ; :: thesis:
let F be Dependency-set of X; :: thesis:

hereby :: thesis:

assume that
A1: F is (F1) and
A2: F is (F2) and
A3: F is (F3) and
A4: F is (F4) ; :: thesis:
thus F is (F2) by A2; :: thesis:
thus F is (DC3) by A1, A3; :: thesis:
thus F is (DC4) :: thesis:

proof

let A, B, C be Subset of X; :: according to ARMSTRNG:def 29 :: thesis:
assume that
A5: [A,B] in F and
A6: [A,C] in F ; :: thesis:
[(A \/ A),(B \/ C)] in F by A4, A5, A6, Def14;
hence [A,(B \/ C)] in F ; :: thesis:

end;

end;

assume that
A7: F is (F2) and
A8: F is (DC3) and
A9: F is (DC4) ; :: thesis:
thus F is (F1) by A7, A8; :: thesis:
thus F is (F2) by A7; :: thesis:
thus F is (F3) by A7, A8; :: thesis:
let A, B, A', B' be Subset of X; :: according to ARMSTRNG:def 14 :: thesis:
assume that
A10: [A,B] in F and
A11: [A',B'] in F ; :: thesis:
A' c= A \/ A' by XBOOLE_1:7;
then [(A \/ A'),A'] in F by A8, Def16;
then A12: [(A \/ A'),B'] in F by A7, A11, Th20;
A c= A \/ A' by XBOOLE_1:7;
then [(A \/ A'),A] in F by A8, Def16;
then [(A \/ A'),B] in F by A7, A10, Th20;
hence [(A \/ A'),(B \/ B')] in F by A9, A12, Def29; :: thesis: