let S be Language; :: thesis: for phi1, phi2 being wff string of S holds
( Depth ((<*()*> ^ phi1) ^ phi2) > Depth phi1 & Depth ((<*()*> ^ phi1) ^ phi2) > Depth phi2 )

let phi1, phi2 be wff string of S; :: thesis: ( Depth ((<*()*> ^ phi1) ^ phi2) > Depth phi1 & Depth ((<*()*> ^ phi1) ^ phi2) > Depth phi2 )
set nor = TheNorSymbOf S;
set phi = (<*()*> ^ phi1) ^ phi2;
set m1 = Depth phi1;
set m2 = Depth phi2;
set M = Depth ((<*()*> ^ phi1) ^ phi2);
set L = LettersOf S;
set FF = AllFormulasOf S;
set SS = AllSymbolsOf S;
consider n being Nat such that
B0: Depth ((<*()*> ^ phi1) ^ phi2) = n + 1 by NAT_1:6;
set Phin = S -formulasOfMaxDepth n;
(<*()*> ^ phi1) ^ phi2 in n -NorFormulasOf S by ;
then consider phi11, phi22 being Element of S -formulasOfMaxDepth n such that
B1: (<*()*> ^ phi1) ^ phi2 = (<*()*> ^ phi11) ^ phi22 ;
reconsider phi111 = phi11, phi222 = phi22 as n -wff string of S by Def23;
<*()*> ^ (phi1 ^ phi2) = (<*()*> ^ phi1) ^ phi2 by FINSEQ_1:32
.= <*()*> ^ (phi11 ^ phi22) by ;
then B2: phi1 ^ phi2 = phi111 ^ phi222 by FINSEQ_1:33;
( phi111 in AllFormulasOf S & phi1 in AllFormulasOf S ) by Th16;
then ( phi1 is n -wff & phi2 is n -wff ) by ;
then ( Depth phi1 <= n & Depth phi2 <= n ) by Def30;
then ( (Depth phi1) + 0 < n + 1 & (Depth phi2) + 0 < n + 1 ) by XREAL_1:8;
hence ( Depth ((<*()*> ^ phi1) ^ phi2) > Depth phi1 & Depth ((<*()*> ^ phi1) ^ phi2) > Depth phi2 ) by B0; :: thesis: verum