let F be Dependency-set of X; :: thesis: ( F is (F1) & F is (F3) implies F is (DC3) )
assume A1: ( F is (F1) & F is (F3) ) ; :: thesis: F is (DC3)
let A, B be Subset of X; :: according to ARMSTRNG:def 16 :: thesis: ( B c= A implies [A,B] in F )
assume A2: B c= A ; :: thesis: [A,B] in F
A3: [A,A] in F by A1, Def12;
[A,A] >= [A,B] by A2, Th15;
hence [A,B] in F by A1, A3, Def13; :: thesis: verum