set IT = m -NorFormulasOf S;
set Phim = S -formulasOfMaxDepth m;
set F = S -firstChar ;
set N = TheNorSymbOf S;
set SS = AllSymbolsOf S;
let x be Element of m -NorFormulasOf S; :: thesis: not x is exal
x in m -NorFormulasOf S ;
then consider phi1, phi2 being Element of S -formulasOfMaxDepth m such that
A1: x = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 ;
reconsider phi = x as string of S ;
(S -firstChar) . phi = phi . 1 by FOMODEL0:6
.= (<*(TheNorSymbOf S)*> ^ (phi1 ^ phi2)) . 1 by FINSEQ_1:32, A1
.= TheNorSymbOf S by FINSEQ_1:41 ;
hence not x is exal ; :: thesis: verum