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 A is_properly_applicable_to t holds
T @--> reduces A ast t,t