:: deftheorem defines AtomicFormulasOf FOMODEL1:def 36 :
for S being Language holds AtomicFormulasOf S = { phi where phi is string of S : phi is 0wff } ;