let F be Dependency-set of X; :: thesis: ( F is (DC3) & F is (F2) implies ( F is (F1) & F is (F3) ) )
assume A3: ( F is (DC3) & F is (F2) ) ; :: thesis: ( F is (F1) & F is (F3) )
thus F is (F1) :: thesis: F is (F3)

proof

let A be Subset of X; :: according to ARMSTRNG:def 12 :: thesis: [A,A] in F
thus [A,A] in F by A3, Def16; :: thesis: verum

end;

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 A4: [A,B] in F ; :: thesis: ( not [A,B] >= [A',B'] or [A',B'] in F )
assume A5: [A,B] >= [A',B'] ; :: thesis: [A',B'] in F
then A c= A' by Th15;
then [A',A] in F by A3, Def16;
then A6: [A',B] in F by A3, A4, Th20;
B' c= B by A5, Th15;
then [B,B'] in F by A3, Def16;
hence [A',B'] in F by A3, A6, Th20; :: thesis: verum