set L = LettersOf S;
set P = OpSymbolsOf S;
set T = TermSymbolsOf S;
set f = the adicity of S;
let s be termal Element of S; :: thesis: ( not s is literal implies s is operational )
A1: s in TermSymbolsOf S by Def18;
assume not s is literal ; :: thesis: s is operational
then not s in LettersOf S ;
then ( s in (TermSymbolsOf S) \ (LettersOf S) & (TermSymbolsOf S) \ (LettersOf S) = OpSymbolsOf S ) by FUNCT_1:69, A1, XBOOLE_0:def 5;
hence s is operational ; :: thesis: verum