theorem :: ABCMIZ_0:30

for T being non empty reflexive transitive non void TA-structure
for t being type of T holds (<*> the adjectives of T) ast t = t by Def19;