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