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