:: deftheorem Def12 defines (F3) ARMSTRNG:def 12 :
for X being set
for F being Dependency-set of X holds
( F is (F3) iff for A, B, A9, B9 being Subset of X st [A,B] in F & [A,B] >= [A9,B9] holds
[A9,B9] in F );