let i be Element of SCMPDS-Instr ; :: thesis: ( InsCode i = 14 implies JumpPart i = {} )
assume InsCode i = 14 ; :: thesis: JumpPart i = {}
then i in { [14,{},<*l*>] where l is Element of INT : verum } by Th8;
then ex l being Element of INT st i = [14,{},<*l*>] ;
hence JumpPart i = {} ; :: thesis: verum