let T1, T2 be TA-structure ; :: thesis: ( 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 #) implies for a1 being adjective of T1
for a2 being adjective of T2 st a1 = a2 holds
types a1 = types a2 )
assume A1: 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 #) ; :: thesis: for a1 being adjective of T1
for a2 being adjective of T2 st a1 = a2 holds
types a1 = types a2
let a1 be adjective of T1; :: thesis: for a2 being adjective of T2 st a1 = a2 holds
types a1 = types a2
let a2 be adjective of T2; :: thesis: ( a1 = a2 implies types a1 = types a2 )
assume A2: a1 = a2 ; :: thesis: types a1 = types a2

now :: thesis: ( types a1 is Subset of T2 & ( for x being object holds
( ( x in types a1 implies ex t2 being type of T2 st
( x = t2 & a2 in adjs t2 ) ) & ( ex t2 being type of T2 st
( x = t2 & a2 in adjs t2 ) implies x in types a1 ) ) ) )

thus types a1 is Subset of T2 by A1; :: thesis: for x being object holds
( ( x in types a1 implies ex t2 being type of T2 st
( x = t2 & a2 in adjs t2 ) ) & ( ex t2 being type of T2 st
( x = t2 & a2 in adjs t2 ) implies x in types a1 ) )
let x be object ; :: thesis: ( ( x in types a1 implies ex t2 being type of T2 st
( x = t2 & a2 in adjs t2 ) ) & ( ex t2 being type of T2 st
( x = t2 & a2 in adjs t2 ) implies x in types a1 ) )

hereby :: thesis: ( ex t2 being type of T2 st
( x = t2 & a2 in adjs t2 ) implies x in types a1 )

assume x in types a1 ; :: thesis: ex t2 being type of T2 st
( x = t2 & a2 in adjs t2 )
then consider t1 being type of T1 such that
A3: x = t1 and
A4: a1 in adjs t1 by Def12;
reconsider t2 = t1 as type of T2 by A1;
adjs t1 = adjs t2 by A1;
hence ex t2 being type of T2 st
( x = t2 & a2 in adjs t2 ) by A2, A3, A4; :: thesis: verum

end;

given t2 being type of T2 such that A5: x = t2 and
A6: a2 in adjs t2 ; :: thesis: x in types a1
reconsider t1 = t2 as type of T1 by A1;
adjs t1 = adjs t2 by A1;
hence x in types a1 by A2, A5, A6, Def12; :: thesis: verum

end;

hence types a1 = types a2 by Def12; :: thesis: verum