:: deftheorem defines AtomicFormulaSymbolsOf FOMODEL1:def 10 :
for S being Language-like holds AtomicFormulaSymbolsOf S = (AllSymbolsOf S) \ {(TheNorSymbOf S)};