let R be good Ring; :: thesis: for a being Data-Location of R holds a <> IC (SCM R)
let a be Data-Location of R; :: thesis: a <> IC (SCM R)
a in the carrier of (SCM R) \ (NAT \/ {NAT }) by SCMRING2:def 2;
then not a in NAT \/ {NAT } by XBOOLE_0:def 5;
then not a in {NAT } by XBOOLE_0:def 3;
then a <> NAT by TARSKI:def 1;
hence a <> IC (SCM R) by SCMRING2:9; :: thesis: verum