theorem :: ARMSTRNG:22

for X being set
for F being Dependency-set of X st F is (F1) & F is (F3) holds
F is (DC3) ;