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
B0: 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, B0;
then consider phi11, phi22 being Element of S -formulasOfMaxDepth n such that
B1: (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 = (<*(TheNorSymbOf S)*> ^ phi11) ^ phi22 ;
reconsider phi111 = phi11, phi222 = phi22 as n -wff string of S by Def23;
<*(TheNorSymbOf S)*> ^ (phi1 ^ phi2) = (<*(TheNorSymbOf S)*> ^ phi1) ^ phi2 by FINSEQ_1:32
.= <*(TheNorSymbOf S)*> ^ (phi11 ^ phi22) by B1, FINSEQ_1:32 ;
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 FOMODEL0:def 19, B2;
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 ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) > Depth phi1 & Depth ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) > Depth phi2 ) by B0; :: thesis: verum