set IT = m -NorFormulasOf S;
set Phim = S -formulasOfMaxDepth m;
set N = TheNorSymbOf S;
set SS = AllSymbolsOf S;

now

let x be set ; :: thesis: ( x in m -NorFormulasOf S implies x in ((AllSymbolsOf S) *) \ {{}} )
assume x in m -NorFormulasOf S ; :: thesis: x in ((AllSymbolsOf S) *) \ {{}}
then consider phi1, phi2 being Element of S -formulasOfMaxDepth m such that
C0: x = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 ;
thus x in ((AllSymbolsOf S) *) \ {{}} by C0; :: thesis: verum

end;

hence m -NorFormulasOf S is Subset of (((AllSymbolsOf S) *) \ {{}}) by TARSKI:def 3; :: thesis: verum