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
set s = the State of S;
NIC (i,(IC the State of S)) = {(succ (IC the State of S))} by A1, Th41;
then NIC (i,(IC the State of S)) <> {(IC the State of S)} by ORDINAL1:9, ZFMISC_1:3;
hence not i is halting by Th15; :: thesis: verum