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

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