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 by Def18;
then s in (LowerCompoundersOf S) /\ (TermSymbolsOf S) by A1, XBOOLE_0:def 4;
then s in OpSymbolsOf S by Th1;
hence s is operational by Def16; :: thesis: verum