theorem Th12: :: SCMRING3:13

for R being Ring
for I being Instruction of (SCM R) st InsCode I = 1 holds
ex a, b being Data-Location of R st I = a := b