:: deftheorem defines Dependencies-Order ARMSTRNG:def 10 :
for X being set holds Dependencies-Order X = { [P,Q] where P, Q is Dependency of X : P <= Q } ;