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