let N be with_non-empty_elements set ; :: thesis: for i being Element of the Instructions of (STC N) holds JUMP i is empty
let i be Element of the Instructions of (STC N); :: thesis: JUMP i is empty

per cases ( InsCode i = 1 or InsCode i = 0 ) by Th22;

suppose A1: InsCode i = 1 ; :: thesis: JUMP i is empty

set X = { (NIC i,l) where l is Instruction-Location of STC N : verum } ;
assume not JUMP i is empty ; :: thesis: contradiction
then consider x being set such that
A2: x in meet { (NIC i,l) where l is Instruction-Location of STC N : verum } by XBOOLE_0:def 1;
reconsider l1 = 0 , l2 = 1 as Instruction-Location of STC N by AMI_1:def 4;
( NIC i,l1 in { (NIC i,l) where l is Instruction-Location of STC N : verum } & NIC i,l2 in { (NIC i,l) where l is Instruction-Location of STC N : verum } ) ;
then ( {(0 + 1)} in { (NIC i,l) where l is Instruction-Location of STC N : verum } & {(1 + 1)} in { (NIC i,l) where l is Instruction-Location of STC N : verum } ) by A1, Lm5;
then ( x in {1} & x in {2} ) by A2, SETFAM_1:def 1;
then ( x = 1 & x = 2 ) by TARSKI:def 1;
hence contradiction ; :: thesis: verum

end;

suppose A3: InsCode i = 0 ; :: thesis: JUMP i is empty

reconsider i = i as Instruction of (STC N) ;
for l being Instruction-Location of STC N holds NIC i,l = {l} by A3, Th15, Th20;
hence JUMP i is empty by Th14; :: thesis: verum

end;

end;