theorem Th13: :: SCMRING3:14

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