:: deftheorem Def11 defines (F1) ARMSTRNG:def 11 :
for X being set
for F being Dependency-set of X holds
( F is (F1) iff for A being Subset of X holds [A,A] in F );