theorem Th16: :: SCMRING3:17

for R being Ring
for I being Instruction of (SCM R) st InsCode I = 5 holds
ex a being Data-Location of R ex r being Element of R st I = a := r