let n be Element of NAT ; :: thesis: ( n <= 3 implies n is State of U3(n)Turing )
assume A1: n <= 3 ; :: thesis: n is State of U3(n)Turing
the FStates of U3(n)Turing = SegM 3 by Def21;
hence n is State of U3(n)Turing by A1, Th1; :: thesis: verum