theorem Th7: :: SCMPDS_2:10

for x being set
for d2 being Element of SCM-Data-Loc
for k3, k4 being Integer st x in {4,5,6,7,8} holds
[x,{},<*d2,k3,k4*>] in SCMPDS-Instr