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