let IL be non empty set ; :: thesis: for N being with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N
for i being Instruction of S
for l being Instruction-Location of S holds JUMP i c= NIC i,l
let N be with_non-empty_elements set ; :: thesis: for S being non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N
for i being Instruction of S
for l being Instruction-Location of S holds JUMP i c= NIC i,l
let S be non empty stored-program IC-Ins-separated definite AMI-Struct of IL,N; :: thesis: for i being Instruction of S
for l being Instruction-Location of S holds JUMP i c= NIC i,l
let i be Instruction of S; :: thesis: for l being Instruction-Location of S holds JUMP i c= NIC i,l
let l be Instruction-Location of S; :: thesis: JUMP i c= NIC i,l
set X = { (NIC i,k) where k is Instruction-Location of S : verum } ;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in JUMP i or x in NIC i,l )
assume A1: x in JUMP i ; :: thesis: x in NIC i,l
NIC i,l in { (NIC i,k) where k is Instruction-Location of S : verum } ;
hence x in NIC i,l by A1, SETFAM_1:def 1; :: thesis: verum