theorem Th49: :: ABCMIZ_0:49

for T being reflexive transitive antisymmetric with_suprema Noetherian adj-structured TA-structure
for t being type of T
for A being Subset of the adjectives of T st A is_applicable_to t holds
A ast t <= t