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

now :: thesis: for m being Nat st <*l*> ^ phi1 is m -wff holds
not m < (Depth phi1) + 1

let m be Nat; :: thesis: ( <*l*> ^ phi1 is m -wff implies not m < (Depth phi1) + 1 )
assume C0: <*l*> ^ phi1 is m -wff ; :: thesis: not m < (Depth phi1) + 1
assume m < (Depth phi1) + 1 ; :: thesis: contradiction
then m <= Depth phi1 by NAT_1:13;
then m - m <= (Depth phi1) - m by XREAL_1:13;
then reconsider k = (Depth phi1) - m as Nat ;
<*l*> ^ phi1 is m + (0 * k) -wff by C0;
then <*l*> ^ phi1 is m + k -wff ;
hence contradiction ; :: thesis: verum

end;

hence Depth (<*l*> ^ phi1) = (Depth phi1) + 1 by Def30; :: thesis: verum