set nor = TheNorSymbOf S;
set phi = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2;
set m1 = Depth phi1;
set m2 = Depth phi2;
set m = Depth ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2);
set M = max ((Depth phi1),(Depth phi2));
Depth ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) = (max ((Depth phi1),(Depth phi2))) + 1 by Lm31;
then Depth ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) > (max ((Depth phi1),(Depth phi2))) + 0 by XREAL_1:8;
hence for b₁ being string of S st b₁ = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 holds
not b₁ is max ((Depth phi1),(Depth phi2)) -wff by Def30; :: thesis: verum