theorem Th21: :: ABCMIZ_0:21

for T being reflexive transitive antisymmetric with_suprema Noetherian adj-structured TA-structure
for t being type of T
for a being adjective of T st a is_applicable_to t holds
a in adjs (a ast t)