theorem Th11: :: ABCMIZ_0:11

for T1, T2 being TA-structure st TA-structure(# the carrier of T1, the adjectives of T1, the InternalRel of T1, the non-op of T1, the adj-map of T1 #) = TA-structure(# the carrier of T2, the adjectives of T2, the InternalRel of T2, the non-op of T2, the adj-map of T2 #) holds
for a1 being adjective of T1
for a2 being adjective of T2 st a1 = a2 holds
types a1 = types a2