let I be Instruction of SCMPDS; :: thesis: ( not I in { [I1,{},<*d1,k1,k2*>] where I1 is Element of Segm 15, d1 is Element of SCM-Data-Loc , k1, k2 is Element of INT : I1 in {4,5,6,7,8} } or InsCode I = 4 or InsCode I = 5 or InsCode I = 6 or InsCode I = 7 or InsCode I = 8 )
assume I in { [I1,{},<*d1,k1,k2*>] where I1 is Element of Segm 15, d1 is Element of SCM-Data-Loc , k1, k2 is Element of INT : I1 in {4,5,6,7,8} } ; :: thesis: ( InsCode I = 4 or InsCode I = 5 or InsCode I = 6 or InsCode I = 7 or InsCode I = 8 )
then consider I1 being Element of Segm 15, d1 being Element of SCM-Data-Loc , k1, k2 being Element of INT such that
A1: I = [I1,{},<*d1,k1,k2*>] and
A2: I1 in {4,5,6,7,8} ;
( I1 = 4 or I1 = 5 or I1 = 6 or I1 = 7 or I1 = 8 ) by A2, ENUMSET1:def 3;
hence ( InsCode I = 4 or InsCode I = 5 or InsCode I = 6 or InsCode I = 7 or InsCode I = 8 ) by A1; :: thesis: verum