let S be Language; :: thesis: for phi1, phi2 being wff string of S holds Depth ((<*()*> ^ phi1) ^ phi2) = (max ((Depth phi1),(Depth phi2))) + 1
let phi1, phi2 be wff string of S; :: thesis: Depth ((<*()*> ^ phi1) ^ phi2) = (max ((Depth phi1),(Depth phi2))) + 1
set nor = TheNorSymbOf S;
set phi = (<*()*> ^ phi1) ^ phi2;
set m1 = Depth phi1;
set m2 = Depth phi2;
set m = max ((Depth phi1),(Depth phi2));
set M = Depth ((<*()*> ^ phi1) ^ phi2);
( Depth ((<*()*> ^ phi1) ^ phi2) <= Depth ((<*()*> ^ phi1) ^ phi2) & Depth ((<*()*> ^ phi1) ^ phi2) > Depth phi1 & Depth ((<*()*> ^ phi1) ^ phi2) > Depth phi2 ) by Lm30;
then Depth ((<*()*> ^ phi1) ^ phi2) > max ((Depth phi1),(Depth phi2)) by XXREAL_0:def 10;
then B1: (max ((Depth phi1),(Depth phi2))) + 1 <= Depth ((<*()*> ^ phi1) ^ phi2) by NAT_1:13;
reconsider mm = max ((Depth phi1),(Depth phi2)) as Nat by XXREAL_0:16;
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 Def30;
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 ;
J1: now :: thesis: for n being Nat st (<*()*> ^ phi1) ^ phi2 is n -wff holds
n >= (max ((Depth phi1),(Depth phi2))) + 1
let n be Nat; :: thesis: ( (<*()*> ^ phi1) ^ phi2 is n -wff implies n >= (max ((Depth phi1),(Depth phi2))) + 1 )
assume (<*()*> ^ phi1) ^ phi2 is n -wff ; :: thesis: n >= (max ((Depth phi1),(Depth phi2))) + 1
then n >= Depth ((<*()*> ^ phi1) ^ phi2) by Def30;
hence n >= (max ((Depth phi1),(Depth phi2))) + 1 by ; :: thesis: verum
end;
set Phim = S -formulasOfMaxDepth mm;
set NF = mm -NorFormulasOf S;
set PhiM = S -formulasOfMaxDepth (mm + 1);
set EF = mm -ExFormulasOf S;
reconsider phi111 = phi11, phi222 = phi22 as Element of S -formulasOfMaxDepth mm by Def23;
(<*()*> ^ phi1) ^ phi2 = (<*()*> ^ phi111) ^ phi222 ;
then (<*()*> ^ phi1) ^ phi2 in mm -NorFormulasOf S ;
then (<*()*> ^ phi1) ^ phi2 in (() \/ ()) \/ () by Lm8;
then reconsider ITT = (<*()*> ^ phi1) ^ phi2 as Element of S -formulasOfMaxDepth (mm + 1) by Th9;
ITT is (max ((Depth phi1),(Depth phi2))) + 1 -wff ;
then (<*()*> ^ phi11) ^ phi22 is (max ((Depth phi1),(Depth phi2))) + 1 -wff string of S ;
hence Depth ((<*()*> ^ phi1) ^ phi2) = (max ((Depth phi1),(Depth phi2))) + 1 by ; :: thesis: verum