consider
m
being
Nat
such that
A1
:
Depth
phi
=
m
+
1
by
NAT_1:6
;
consider
phi2
being
m
-wff
string
of
S
such that
A2
:
tail
phi
=
phi2
by
A1
,
Lm38
;
thus
tail
phi
is
wff
string
of
S
by
A2
;
:: thesis:
verum