for S being Language
for l being literal Element of S
for phi1, phi2 being wff string of S holds
( Depth (<*l*> ^ phi1) > Depth phi1 & Depth ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) > Depth phi1 & Depth ((<*(TheNorSymbOf S)*> ^ phi1) ^ phi2) > Depth phi2 ) by Lm28, Lm30;