set SS = AllSymbolsOf S;
<*s*> is non empty FinSequence of AllSymbolsOf S ;
hence <*s*> is string of S by FOMODEL0:5; :: thesis: verum