theorem :: ARMSTRNG:54

for X being set
for F being Dependency-set of X holds
( F is (F1) & F is (F2) & F is (F3) & F is (F4) iff ( F is (DC2) & F is (DC5) & F is (DC6) ) )