let R be good Ring; :: thesis: for a being Data-Location of R
for loc being Instruction-Location of SCM R holds a <> loc
let a be Data-Location of R; :: thesis: for loc being Instruction-Location of SCM R holds a <> loc
let loc be Instruction-Location of SCM R; :: thesis: a <> loc
assume a = loc ; :: thesis: contradiction
then loc in the carrier of (SCM R) \ (NAT \/ {NAT }) by SCMRING2:def 2;
then not loc in NAT \/ {NAT } by XBOOLE_0:def 5;
then not loc in NAT by XBOOLE_0:def 3;
hence contradiction by AMI_1:def 4; :: thesis: verum