theorem Th4: :: ABCMIZ_0:4

for a1, a2 being set st a1 <> a2 holds
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 )