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

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