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;
( types a = types b & types (non- a) = types (non- b) & not (types a) \/ (types (non- a)) is empty ) by A1, A2, Th11;
hence not (types b) \/ (types (non- b)) is empty ; :: thesis: verum