:: deftheorem defines is_applicable_to ABCMIZ_0:def 16 :
for T being TA-structure
for t being type of T
for A being Subset of the adjectives of T holds
( A is_applicable_to t iff ex t9 being type of T st
( A c= adjs t9 & t9 <= t ) );