let A1, A2 be AdjectiveStr ; :: thesis: ( AdjectiveStr(# the adjectives of A1, the non-op of A1 #) = AdjectiveStr(# the adjectives of A2, the non-op of A2 #) & A1 is involutive implies A2 is involutive )
assume A1: AdjectiveStr(# the adjectives of A1, the non-op of A1 #) = AdjectiveStr(# the adjectives of A2, the non-op of A2 #) ; :: thesis: ( not A1 is involutive or A2 is involutive )
assume A2: for a being adjective of A1 holds non- (non- a) = a ; :: according to ABCMIZ_0:def 6 :: thesis: A2 is involutive
let a be adjective of A2; :: according to ABCMIZ_0:def 6 :: thesis: non- (non- a) = a
reconsider b = a as adjective of A1 by A1;
thus non- (non- a) = non- (non- b) by A1
.= a by A2 ; :: thesis: verum