set
m
=
Depth
phi
;
set
psi
=
<*
l
*>
^
phi
;
set
M
=
Depth
(
<*
l
*>
^
phi
)
;
reconsider
phii
=
phi
as
Depth
phi
-wff
string
of
S
by
Def30
;
<*
l
*>
^
phii
is
(
Depth
phi
)
+
1
-wff
;
hence
for
b
_{1}
being
string
of
S
st
b
_{1}
=
<*
l
*>
^
phi
holds
b
_{1}
is 1
+
(
Depth
phi
)
-wff
;
:: thesis:
verum