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) by A3; :: thesis: F is (F3)
let A, B, A9, B9 be Subset of X; :: according to ARMSTRNG:def 12 :: 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 ;
then [A9,A] in F by A3;
then A6: [A9,B] in F by A3, A4, Th18;
B9 c= B by A5;
then [B,B9] in F by A3;
hence [A9,B9] in F by A3, A6, Th18; :: thesis: verum