theorem Th3: :: SCM_INST:3

for x being set
for a2 being Nat
for b2 being Element of SCM-Data-Loc st x in {7,8} holds
[x,<*a2*>,<*b2*>] in SCM-Instr