theorem Th52: :: ABCMIZ_0:52

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
for t9 being type of T st t9 <= t & A c= adjs t9 holds
( A is_applicable_to t & t9 <= A ast t )