theorem Th2: :: SCMPDS_9:2

for i being Instruction of SCMPDS st ( for l being Element of NAT holds NIC (i,l) = {(l + 1)} ) holds
JUMP i is empty