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