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:63;
n . x = y by FUNCT_4:63;
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