let S be Language; :: thesis: for l being literal Element of S
for phi1 being wff string of S holds Depth (<*l*> ^ phi1) > Depth phi1
let l be literal Element of S; :: thesis: for phi1 being wff string of S holds Depth (<*l*> ^ phi1) > Depth phi1
let phi1 be wff string of S; :: thesis: Depth (<*l*> ^ phi1) > Depth phi1
set nor = TheNorSymbOf S;
set phi = <*l*> ^ phi1;
set m = Depth phi1;
set M = Depth (<*l*> ^ phi1);
set L = LettersOf S;
consider n being Nat such that
B1: Depth (<*l*> ^ phi1) = n + 1 by NAT_1:6;
set Phin = S -formulasOfMaxDepth n;
<*l*> ^ phi1 in n -ExFormulasOf S by Lm27, B1;
then consider v being Element of LettersOf S, psi being Element of S -formulasOfMaxDepth n such that
B0: <*l*> ^ phi1 = <*v*> ^ psi ;
v = (<*v*> ^ psi) . 1 by FINSEQ_1:41
.= l by B0, FINSEQ_1:41 ;
then psi = phi1 by B0, FINSEQ_1:33;
then phi1 is n -wff ;
then Depth phi1 <= n by Def30;
then (Depth phi1) + 0 < n + 1 by XREAL_1:8;
hence Depth (<*l*> ^ phi1) > Depth phi1 by B1; :: thesis: verum