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

now :: thesis: for x being object st x in m -NorFormulasOf S holds
x in ((AllSymbolsOf S) *) \ {{}}

let x be object ; :: thesis: ( x in m -NorFormulasOf S implies x in ((AllSymbolsOf S) *) \ {{}} )
assume x in m -NorFormulasOf S ; :: thesis: x in ((AllSymbolsOf S) *) \ {{}}
then ex phi1, phi2 being Element of S -formulasOfMaxDepth m st x = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 ;
hence x in ((AllSymbolsOf S) *) \ {{}} ; :: thesis: verum

end;

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