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 )
A1: n . y = x by FUNCT_4:66;
n . x = y 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 A1, Th4; :: thesis: verum