set E = m -ExFormulasOf S;
set L = LettersOf S;
set Phim = S -formulasOfMaxDepth m;
let x be Element of m -ExFormulasOf S; :: thesis: x is exal
x in m -ExFormulasOf S ;
then consider l being Element of LettersOf S, phi being Element of S -formulasOfMaxDepth m such that
A1: x = <*l*> ^ phi ;
thus x is exal by A1; :: thesis: verum