theorem :: ABCMIZ_0:38

for T being non empty reflexive transitive non void TA-structure
for t being type of T holds <*> the adjectives of T is_applicable_to t ;