set L = LettersOf S;
set P = OpSymbolsOf S;
set O = OwnSymbolsOf S;
set T = TermSymbolsOf S;
A1: (TermSymbolsOf S) \ (LettersOf S) = OpSymbolsOf S by FUNCT_1:69;
let s be own Element of S; :: thesis: ( not s is low-compounding implies s is literal )
reconsider ss = s as ofAtomicFormula Element of S ;
assume A2: not s is low-compounding ; :: thesis: s is literal
then not ss is relational ;
then reconsider sss = ss as termal ofAtomicFormula Element of S ;
assume not s is literal ; :: thesis: contradiction
then ( sss in TermSymbolsOf S & not s in LettersOf S ) by Def18;
then s in (TermSymbolsOf S) \ (LettersOf S) by XBOOLE_0:def 5;
then ( s is operational & not s is operational ) by A2, A1;
hence contradiction ; :: thesis: verum