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