set l = the literal Element of S;
consider m being Nat such that
A1: m1 = m + 1 by NAT_1:6;
set phi = the m -wff string of S;
reconsider psi = <* the literal Element of S*> ^ the m -wff string of S as m1 -wff exal string of S by A1;
take psi ; :: thesis: not psi is 0wff
thus not psi is 0wff ; :: thesis: verum