for T being non empty reflexive transitive non void TAS-structure
for t being type of T
for a being adjective of T holds
( a is_properly_applicable_to t iff <*a*> is_properly_applicable_to t )