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