:: deftheorem defines ast ABCMIZ_0:def 17 :
for T being non empty reflexive transitive TA-structure
for t being Element of T
for a being adjective of T holds a ast t = sup ((types a) /\ (downarrow t));