set IT = m -ExFormulasOf S;
set SS = AllSymbolsOf S;
set Phim = S -formulasOfMaxDepth m;
set L = LettersOf S;

now

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

end;

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