let s be Element of S; :: thesis: ( s is literal implies s is termal )
assume s is literal ; :: thesis: s is termal
then ( LettersOf S c= TermSymbolsOf S & s in LettersOf S ) by Th1;
hence s is termal ; :: thesis: verum