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