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