theorem Th31: :: ABCMIZ_0:31

for T being non empty reflexive transitive non void TA-structure
for t being type of T
for a being adjective of T holds <*a*> ast t = a ast t