let S be 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
let x be 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
let R be Ring; for d1, d2 being Data-Location of R st x in {1,2,3,4} holds
[x,{},<*d1,d2*>] in SCM-Instr S
let d1, d2 be Data-Location of R; ( x in {1,2,3,4} implies [x,{},<*d1,d2*>] in SCM-Instr S )
reconsider d1 = d1, d2 = d2 as Element of SCM-Data-Loc by Th1, AMI_3:27;
( x in {1,2,3,4} implies [x,{},<*d1,d2*>] in SCM-Instr S )
by SCMRINGI:8;
hence
( x in {1,2,3,4} implies [x,{},<*d1,d2*>] in SCM-Instr S )
; verum