set s = the Element of LettersOf S;
take the Element of LettersOf S ; :: thesis: the Element of LettersOf S is literal
thus the Element of LettersOf S is literal ; :: thesis: verum