theorem :: ARMSTRNG:53

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 (DC1) & F is (DC3) & F is (DC4) ) )