theorem :: ARMSTRNG:14

for X, x being set holds
( x in Dependencies-Order X iff ex P, Q being Dependency of X st
( x = [P,Q] & P <= Q ) ) ;