let N be non empty 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

reconsider l1 = 0 , l2 = 1 as Element of NAT ;
set X = { (NIC i,l) where l is Element of NAT : 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 Element of NAT : verum } by XBOOLE_0:def 1;
NIC i,l1 in { (NIC i,l) where l is Element of NAT : verum } ;
then {(0 + 1)} in { (NIC i,l) where l is Element of NAT : verum } by A1, Lm5;
then x in {1} by A2, SETFAM_1:def 1;
then A3: x = 1 by TARSKI:def 1;
NIC i,l2 in { (NIC i,l) where l is Element of NAT : verum } ;
then {(1 + 1)} in { (NIC i,l) where l is Element of NAT : verum } by A1, Lm5;
then x in {2} by A2, SETFAM_1:def 1;
hence contradiction by A3, TARSKI:def 1; :: thesis: verum

end;

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

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

end;

end;