let s be Element of S; :: thesis: ( s is operational implies s is termal )
assume s is operational ; :: thesis: s is termal
then ( s in OpSymbolsOf S & OpSymbolsOf S c= TermSymbolsOf S ) by Lm8, DefOperational;
hence s is termal by DefTermal0; :: thesis: verum