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

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

let x be object ; :: thesis: ( x in m -ExFormulasOf S implies x in ((AllSymbolsOf S) *) \ {{}} )
assume x in m -ExFormulasOf S ; :: thesis: x in ((AllSymbolsOf S) *) \ {{}}
then ex l being Element of LettersOf S ex phi being Element of S -formulasOfMaxDepth m st x = <*l*> ^ phi ;
hence x in ((AllSymbolsOf S) *) \ {{}} ; :: thesis: verum

end;

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