let I be Instruction of (STC N); :: according to AMISTD_2:def 2 :: thesis: I is with_explicit_jumps
thus JUMP I = rng (JumpPart I) ; :: according to AMISTD_2:def 1 :: thesis: verum