let S be Language; :: thesis: for phi1, phi2 being wff string of S holds Depth ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) = (max ((Depth phi1),(Depth phi2))) + 1
let phi1, phi2 be wff string of S; :: thesis: Depth ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) = (max ((Depth phi1),(Depth phi2))) + 1
set nor = TheNorSymbOf S;
set phi = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2;
set m1 = Depth phi1;
set m2 = Depth phi2;
set m = max ((Depth phi1),(Depth phi2));
set M = Depth ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2);
( Depth ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) <= Depth ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) & Depth ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) > Depth phi1 & Depth ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) > Depth phi2 ) by Lm30;
then Depth ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) > max ((Depth phi1),(Depth phi2)) by XXREAL_0:def 10;
then A1: (max ((Depth phi1),(Depth phi2))) + 1 <= Depth ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) by NAT_1:13;
reconsider d1 = (max ((Depth phi1),(Depth phi2))) - (Depth phi1), d2 = (max ((Depth phi1),(Depth phi2))) - (Depth phi2) as Nat ;
( phi1 is (Depth phi1) + (0 * d1) -wff & phi2 is (Depth phi2) + (0 * d2) -wff ) by Def31;
then ( phi1 is (Depth phi1) + d1 -wff & phi2 is (Depth phi2) + d2 -wff ) ;
then reconsider phi11 = phi1, phi22 = phi2 as max ((Depth phi1),(Depth phi2)) -wff string of S ;
thus Depth ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) = (max ((Depth phi1),(Depth phi2))) + 1 by Def31; :: thesis: verum