:: deftheorem Def14 defines full_family ARMSTRNG:def 14 :
for X being set
for F being Dependency-set of X holds
( F is full_family iff ( F is (F1) & F is (F2) & F is (F3) & F is (F4) ) );