consider
m
being
Nat
such that
A1
:
phi
is
m
-wff
by
Def24
;
reconsider
phii
=
phi
as
m
-wff
string
of
S
by
A1
;
set
IT
=
<*
l
*>
^
phii
;
<*
l
*>
^
phii
is
m
+
1
-wff
;
hence
for
b
_{1}
being
string
of
S
st
b
_{1}
=
<*
l
*>
^
phi
holds
b
_{1}
is
wff
;
:: thesis:
verum