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 15 :: thesis: ( B c= A implies [A,B] in F )
assume B c= A ; :: thesis: [A,B] in F
then A2: [A,A] >= [A,B] ;
thus [A,B] in F by A1, A2; :: thesis: verum