set L = LowerCompoundersOf S;
set T = TermSymbolsOf S;
set OP = OpSymbolsOf S;
let s be low-compounding Element of S; :: thesis: ( s is termal implies s is operational )
A1: s in LowerCompoundersOf S by Def15;
assume s is termal ; :: thesis: s is operational
then s in TermSymbolsOf S ;
then s in (LowerCompoundersOf S) /\ (TermSymbolsOf S) by XBOOLE_0:def 4, A1;
then s in OpSymbolsOf S by Th1;
hence s is operational ; :: thesis: verum