:: deftheorem defines is_properly_applicable_to ABCMIZ_0:def 29 :
for T being non empty reflexive transitive non void TAS-structure
for t being type of T
for A being Subset of the adjectives of T holds
( A is_properly_applicable_to t iff ex s being FinSequence of the adjectives of T st
( rng s = A & s is_properly_applicable_to t ) );