:: deftheorem defines (DC6) ARMSTRNG:def 30 :
for X being set
for F being Dependency-set of X holds
( F is (DC6) iff for A, B, C being Subset of X st [A,B] in F holds
[(A \/ C),B] in F );