let x be set ; :: thesis: for d4, d5 being Element of SCM-Data-Loc
for k5, k6 being Integer st x in {9,10,11,12,13} holds
[x,{},<*d4,d5,k5,k6*>] in SCMPDS-Instr
let d4, d5 be Element of SCM-Data-Loc ; :: thesis: for k5, k6 being Integer st x in {9,10,11,12,13} holds
[x,{},<*d4,d5,k5,k6*>] in SCMPDS-Instr
let k5, k6 be Integer; :: thesis: ( x in {9,10,11,12,13} implies [x,{},<*d4,d5,k5,k6*>] in SCMPDS-Instr )
assume A1: x in {9,10,11,12,13} ; :: thesis: [x,{},<*d4,d5,k5,k6*>] in SCMPDS-Instr
then ( x = 9 or x = 10 or x = 11 or x = 12 or x = 13 ) by ENUMSET1:def 3;
then reconsider x = x as Element of Segm 15 by NAT_1:44;
( k5 is Element of INT & k6 is Element of INT ) by INT_1:def 2;
then [x,{},<*d4,d5,k5,k6*>] in { [I3,{},<*d4,d5,k5,k6*>] where I3 is Element of Segm 15, d4, d5 is Element of SCM-Data-Loc , k5, k6 is Element of INT : I3 in {9,10,11,12,13} } by A1;
hence [x,{},<*d4,d5,k5,k6*>] in SCMPDS-Instr by XBOOLE_0:def 3; :: thesis: verum