theorem Th27: :: ABCMIZ_0:27

for T being non empty reflexive transitive antisymmetric TA-structure
for t being type of T holds ({} the adjectives of T) ast t = t