not the InstructionsF of S is trivial by AMISTD_4:def 1;
then consider x, y being object such that
A1: ( x in the InstructionsF of S & y in the InstructionsF of S ) and
A2: x <> y by ZFMISC_1:def 10;
( x <> halt S or y <> halt S ) by A2;
then consider i being Instruction of S such that
A3: i <> halt S by A1;
take i ; :: thesis: i is No-StopCode
thus i is No-StopCode by A3, COMPOS_0:def 12; :: thesis: verum