:: deftheorem Def13 defines (F4) ARMSTRNG:def 13 :
for X being set
for F being Dependency-set of X holds
( F is (F4) iff for A, B, A9, B9 being Subset of X st [A,B] in F & [A9,B9] in F holds
[(A \/ A9),(B \/ B9)] in F );