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 Th1;
hence s is own ; :: thesis: verum