set L = LettersOf S;
set SS = AllSymbolsOf S;
reconsider Y = (((AllSymbolsOf S) *) \ {{}}) /\ X as FinSequence-membered Subset of X ;
reconsider Z = SymbolsOf Y as finite set ;
reconsider free = (LettersOf S) \ Z as infinite Subset of (LettersOf S) ;
set ll = the Element of free;
reconsider l = the Element of free as literal Element of S by TARSKI:def 3;
take l ; :: thesis: l is X -absent
not l in Z by XBOOLE_0:def 5;
hence l is X -absent ; :: thesis: verum