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 consistent implies T2 is consistent )
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 t being type of T1
for a being adjective of T1 st a in adjs t holds
not non- a in adjs t ; :: according to ABCMIZ_0:def 9 :: thesis: T2 is consistent
let t2 be type of T2; :: according to ABCMIZ_0:def 9 :: thesis: for a being adjective of T2 st a in adjs t2 holds
not non- a in adjs t2
let a2 be adjective of T2; :: thesis: ( a2 in adjs t2 implies not non- a2 in adjs t2 )
reconsider a1 = a2 as adjective of T1 by A1;
reconsider t1 = t2 as type of T1 by A1;
assume a2 in adjs t2 ; :: thesis: not non- a2 in adjs t2
then not non- a1 in adjs t1 by A1, A2;
hence not non- a2 in adjs t2 by A1; :: thesis: verum