:: deftheorem Def15 defines (DC3) ARMSTRNG:def 15 :
for X being set
for F being Dependency-set of X holds
( F is (DC3) iff for A, B being Subset of X st B c= A holds
[A,B] in F );