theorem :: ARMSTRNG:21

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