theorem Th3: :: SCMRING2:3

for S being non empty 1-sorted
for x being set
for R being Ring
for d1, d2 being Data-Location of R st x in {1,2,3,4} holds
[x,{},<*d1,d2*>] in SCM-Instr S