let s be Element of S; :: thesis: ( s is own implies s is ofAtomicFormula )
assume s is own ; :: thesis: s is ofAtomicFormula
then ( s in OwnSymbolsOf S & OwnSymbolsOf S c= AtomicFormulaSymbolsOf S ) by Th1;
hence s is ofAtomicFormula ; :: thesis: verum