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