:: deftheorem defines Maximal_wrt ARMSTRNG:def 16 :
for X being set
for F being Dependency-set of X holds Maximal_wrt F = (Dependencies-Order X) Maximal_in F;