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