set IT = m -ExFormulasOf S;
set L = LettersOf S;
set Phim = S -formulasOfMaxDepth m;
set l = the Element of LettersOf S;
set phi = the Element of S -formulasOfMaxDepth m;
set x = <* the Element of LettersOf S*> ^ the Element of S -formulasOfMaxDepth m;
<* the Element of LettersOf S*> ^ the Element of S -formulasOfMaxDepth m in m -ExFormulasOf S ;
hence for b₁ being set st b₁ = m -ExFormulasOf S holds
not b₁ is empty ; :: thesis: verum