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

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