let i be Instruction of S; :: thesis: ( i is sequential implies not i is halting )
assume A1: i is sequential ; :: thesis: not i is halting
consider s being State of S;
NIC i,(IC s) = {(succ (IC s))} by A1, Th41;
then NIC i,(IC s) <> {(IC s)} by ORDINAL1:14, ZFMISC_1:6;
hence not i is halting by Th15; :: thesis: verum