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 without_fixpoints implies A2 is without_fixpoints )
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 without_fixpoints or A2 is without_fixpoints )
assume A2: for a being adjective of A1 holds not non- a = a ; :: according to ABCMIZ_0:def 7 :: thesis: A2 is without_fixpoints
given a being adjective of A2 such that A3: non- a = a ; :: according to ABCMIZ_0:def 7 :: thesis: contradiction
reconsider b = a as adjective of A1 by A1;
non- b = b by A1, A3;
hence contradiction by A2; :: thesis: verum