let N be with_zero set ; for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for i being Instruction of S
for l being Nat holds JUMP i c= NIC (i,l)
let S be non empty with_non-empty_values IC-Ins-separated AMI-Struct over N; for i being Instruction of S
for l being Nat holds JUMP i c= NIC (i,l)
let i be Instruction of S; for l being Nat holds JUMP i c= NIC (i,l)
let l be Nat; JUMP i c= NIC (i,l)
set X = { (NIC (i,k)) where k is Nat : verum } ;
let x be object ; TARSKI:def 3 ( not x in JUMP i or x in NIC (i,l) )
A1:
NIC (i,l) in { (NIC (i,k)) where k is Nat : verum }
;
assume
x in JUMP i
; x in NIC (i,l)
hence
x in NIC (i,l)
by A1, SETFAM_1:def 1; verum