:: deftheorem defines TheNorSymbOf FOMODEL1:def 8 :
for S being Language-like holds TheNorSymbOf S = the OneF of S;