for T being reflexive transitive antisymmetric with_suprema Noetherian non void adj-structured TA-structure
for t being type of T
for v being FinSequence of the adjectives of T st v is_applicable_to t holds
rng v c= adjs (v ast t)