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