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