for T being non empty reflexive transitive non void TAS-structure
for t being type of T holds {} the adjectives of T is_properly_applicable_to t