:: deftheorem Def20 defines ofAtomicFormula FOMODEL1:def 20 :
for S being Language-like
for s being Element of S holds
( s is ofAtomicFormula iff s in AtomicFormulaSymbolsOf S );