let S be Language; :: thesis: for l being literal Element of S
for phi1, phi2 being wff string of S holds
( Depth ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) = 1 + (max ((Depth phi1),(Depth phi2))) & Depth (<*l*> ^ phi1) = (Depth phi1) + 1 )
let l be literal Element of S; :: thesis: for phi1, phi2 being wff string of S holds
( Depth ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) = 1 + (max ((Depth phi1),(Depth phi2))) & Depth (<*l*> ^ phi1) = (Depth phi1) + 1 )
let phi1, phi2 be wff string of S; :: thesis: ( Depth ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) = 1 + (max ((Depth phi1),(Depth phi2))) & Depth (<*l*> ^ phi1) = (Depth phi1) + 1 )
set N = TheNorSymbOf S;
set m1 = Depth phi1;
set m2 = Depth phi2;
set e = <*l*> ^ phi1;
set n = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2;
thus Depth ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) = 1 + (max ((Depth phi1),(Depth phi2))) by Lm31; :: thesis: Depth (<*l*> ^ phi1) = (Depth phi1) + 1
thus Depth (<*l*> ^ phi1) = (Depth phi1) + 1 by Def31; :: thesis: verum