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

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