set R = RelSymbolsOf S;
set SSS = AtomicFormulaSymbolsOf S;
set T = TermSymbolsOf S;
let s be ofAtomicFormula Element of S; :: thesis: ( not s is relational implies s is termal )
assume not s is relational ; :: thesis: s is termal
then ( s in AtomicFormulaSymbolsOf S & not s in RelSymbolsOf S ) by Def20;
then s in (AtomicFormulaSymbolsOf S) \ (RelSymbolsOf S) by XBOOLE_0:def 5;
then s in TermSymbolsOf S by Th11;
hence s is termal ; :: thesis: verum