:: deftheorem defines ast ABCMIZ_0:def 18 :
for T being non empty reflexive transitive TA-structure
for t being type of T
for A being Subset of the adjectives of T holds A ast t = sup ((types A) /\ (downarrow t));