set phi = the 0 -wff string of S;

set N = TheNorSymbOf S;

set phi1 = (<*(TheNorSymbOf S)*> ^ the 0 -wff string of S) ^ the 0 -wff string of S;

consider m being Nat such that

A1: m1 = m + 1 by NAT_1:6;

(<*(TheNorSymbOf S)*> ^ the 0 -wff string of S) ^ the 0 -wff string of S is non 0wff 1 + (0 * m) -wff string of S ;

then reconsider phi11 = (<*(TheNorSymbOf S)*> ^ the 0 -wff string of S) ^ the 0 -wff string of S as non 0wff m1 -wff string of S by A1;

take phi11 ; :: thesis: not phi11 is exal

thus not phi11 is exal ; :: thesis: verum

set N = TheNorSymbOf S;

set phi1 = (<*(TheNorSymbOf S)*> ^ the 0 -wff string of S) ^ the 0 -wff string of S;

consider m being Nat such that

A1: m1 = m + 1 by NAT_1:6;

(<*(TheNorSymbOf S)*> ^ the 0 -wff string of S) ^ the 0 -wff string of S is non 0wff 1 + (0 * m) -wff string of S ;

then reconsider phi11 = (<*(TheNorSymbOf S)*> ^ the 0 -wff string of S) ^ the 0 -wff string of S as non 0wff m1 -wff string of S by A1;

take phi11 ; :: thesis: not phi11 is exal

thus not phi11 is exal ; :: thesis: verum