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, A9, B9 be Subset of X; :: according to ARMSTRNG:def 13 :: thesis: ( [A,B] in F & [A,B] >= [A9,B9] implies [A9,B9] in F )
assume A4: [A,B] in F ; :: thesis: ( not [A,B] >= [A9,B9] or [A9,B9] in F )
assume A5: [A,B] >= [A9,B9] ; :: thesis: [A9,B9] in F
then A c= A9 by Th15;
then [A9,A] in F by A3, Def16;
then A6: [A9,B] in F by A3, A4, Th20;
B9 c= B by A5, Th15;
then [B,B9] in F by A3, Def16;
hence [A9,B9] in F by A3, A6, Th20; :: thesis: verum