reconsider x = 0 , y = 1 as Element of {0 ,1} by TARSKI:def 2;
reconsider n = 0 ,1 --> y,x as UnOp of {0 ,1} ;
take AdjectiveStr(# {0 ,1},n #) ; :: thesis: ( not AdjectiveStr(# {0 ,1},n #) is void & AdjectiveStr(# {0 ,1},n #) is involutive & AdjectiveStr(# {0 ,1},n #) is without_fixpoints )
( 0 <> 1 & n . x = y & n . y = x ) by FUNCT_4:66;
hence ( not AdjectiveStr(# {0 ,1},n #) is void & AdjectiveStr(# {0 ,1},n #) is involutive & AdjectiveStr(# {0 ,1},n #) is without_fixpoints ) by Th4; :: thesis: verum