for T being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TAS-structure
for t being type of T
for A being finite Subset of the adjectives of T st ( for C being Subset of the adjectives of T st C c= A & C is_properly_applicable_to t & A ast t = C ast t holds
C = A ) holds
for s being one-to-one FinSequence of the adjectives of T st rng s = A & s is_properly_applicable_to t holds
for i being Nat st 1 <= i & i <= len s holds
[((apply (s,t)) . (i + 1)),((apply (s,t)) . i)] in T @-->