let
n
be
Element
of
NAT
;
:: thesis:
(
n
<=
5 implies
n
is
State
of
SumTuring
)
assume
A1
:
n
<=
5 ;
:: thesis:
n
is
State
of
SumTuring
the
FStates
of
SumTuring
=
SegM
5
by
Def14
;
hence
n
is
State
of
SumTuring
by
A1
,
Th1
;
:: thesis:
verum