take the Element of LettersOf S ; :: thesis: the Element of LettersOf S is literal
thus the Element of LettersOf S is literal by Def14; :: thesis: verum