let i be Element of SCM-Instr ; :: thesis: ( ( InsCode i = 1 or InsCode i = 2 or InsCode i = 3 or InsCode i = 4 or InsCode i = 5 ) implies JumpPart i = {} )
assume ( InsCode i = 1 or InsCode i = 2 or InsCode i = 3 or InsCode i = 4 or InsCode i = 5 ) ; :: thesis: JumpPart i = {}
then i in { [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5} } by Th9;
then ex I being Element of Segm 9 ex b, c being Element of SCM-Data-Loc st
( i = [I,{},<*b,c*>] & I in {1,2,3,4,5} ) ;
hence JumpPart i = {} ; :: thesis: verum