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 ( [A,B] in F & [A,C] in F ) ; :: thesis:
then [(A \/ A),(B \/ C)] in F by A4, Def14;
hence [A,(B \/ C)] in F ; :: thesis:

end;

end;

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