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 )
B1: s in LowerCompoundersOf S by DefLowCompounding;
assume s is termal ; :: thesis: s is operational
then s in TermSymbolsOf S by DefTermal0;
then s in (LowerCompoundersOf S) /\ (TermSymbolsOf S) by B1, XBOOLE_0:def 4;
then s in OpSymbolsOf S by Lm8;
hence s is operational by DefOperational; :: thesis: verum