set SS = AllSymbolsOf S;
set A = AtomicTermsOf S;
reconsider L = LettersOf S as Subset of (AllSymbolsOf S) ;
AtomicTermsOf S c= L * by FINSEQ_2:134;
hence AtomicTermsOf S is Subset of ((AllSymbolsOf S) *) by XBOOLE_1:1; :: thesis: verum