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 #) & T1 is adjs-typed implies T2 is adjs-typed )
assume that
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 #) and
A2: for a being adjective of T1 holds not (types a) \/ (types (non- a)) is empty ; :: according to ABCMIZ_0:def 14 :: thesis: T2 is adjs-typed
let b be adjective of T2; :: according to ABCMIZ_0:def 14 :: thesis: not (types b) \/ (types (non- b)) is empty
reconsider a = b as adjective of T1 by A1;
A3: not (types a) \/ (types (non- a)) is empty by A2;
types a = types b by A1, Th11;
hence not (types b) \/ (types (non- b)) is empty by A1, A3, Th11; :: thesis: verum