let s be Element of S; :: thesis: ( s is low-compounding implies s is ofAtomicFormula )
assume s is low-compounding ; :: thesis: s is ofAtomicFormula
then ( s in LowerCompoundersOf S & LowerCompoundersOf S c= AtomicFormulaSymbolsOf S ) by DefLowCompounding;
hence s is ofAtomicFormula by DefOfAtomicFormula; :: thesis: verum