:: deftheorem defines xnot FOMODEL2:def 33 :
for S being Language
for w being string of S holds xnot w = (<*(TheNorSymbOf S)*> ^ w) ^ w;