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