let a1, a2 be set ; :: thesis: ( a1 <> a2 implies for A being AdjectiveStr st the adjectives of A = {a1,a2} & the non-op of A . a1 = a2 & the non-op of A . a2 = a1 holds
( not A is void & A is involutive & A is without_fixpoints ) )
assume A1: a1 <> a2 ; :: thesis: for A being AdjectiveStr st the adjectives of A = {a1,a2} & the non-op of A . a1 = a2 & the non-op of A . a2 = a1 holds
( not A is void & A is involutive & A is without_fixpoints )
let A be AdjectiveStr ; :: thesis: ( the adjectives of A = {a1,a2} & the non-op of A . a1 = a2 & the non-op of A . a2 = a1 implies ( not A is void & A is involutive & A is without_fixpoints ) )
assume that
A2: the adjectives of A = {a1,a2} and
A3: the non-op of A . a1 = a2 and
A4: the non-op of A . a2 = a1 ; :: thesis: ( not A is void & A is involutive & A is without_fixpoints )
thus not the adjectives of A is empty by A2; :: according to ABCMIZ_0:def 4 :: thesis: ( A is involutive & A is without_fixpoints )

hereby :: according to ABCMIZ_0:def 6 :: thesis: A is without_fixpoints

let a be adjective of A; :: thesis: non- (non- a) = a
( a = a1 or a = a2 ) by A2, TARSKI:def 2;
hence non- (non- a) = a by A3, A4; :: thesis: verum

end;

let a be adjective of A; :: according to ABCMIZ_0:def 7 :: thesis: not non- a = a
assume A5: non- a = a ; :: thesis: contradiction
( a = a1 or a = a2 ) by A2, TARSKI:def 2;
hence contradiction by A1, A3, A4, A5; :: thesis: verum