:: deftheorem defines is_applicable_to ABCMIZ_0:def 15 :
for T being TA-structure
for t being Element of T
for a being adjective of T holds
( a is_applicable_to t iff ex t9 being type of T st
( t9 in types a & t9 <= t ) );