:: deftheorem defines (M1) ARMSTRNG:def 18 :
for X being set
for M being Dependency-set of X holds
( M is (M1) iff for A being Subset of X ex A9, B9 being Subset of X st
( [A9,B9] >= [A,A] & [A9,B9] in M ) );