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 )
B1: s in TermSymbolsOf S by DefTermal0;
assume not s is literal ; :: thesis: s is operational
then not s in LettersOf S by DefLiteral;
then ( s in (TermSymbolsOf S) \ (LettersOf S) & (TermSymbolsOf S) \ (LettersOf S) = OpSymbolsOf S ) by B1, FUNCT_1:69, XBOOLE_0:def 5;
hence s is operational by DefOperational; :: thesis: verum