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

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