set IT = m -NorFormulasOf S;
set Phim = S -formulasOfMaxDepth m;
set N = TheNorSymbOf S;
set phi1 = the Element of S -formulasOfMaxDepth m;
set phi2 = the Element of S -formulasOfMaxDepth m;
(<*(TheNorSymbOf S)*> ^ the Element of S -formulasOfMaxDepth m) ^ the Element of S -formulasOfMaxDepth m in m -NorFormulasOf S ;
hence for b₁ being set st b₁ = m -NorFormulasOf S holds
not b₁ is empty ; :: thesis: verum