let R be 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;
then o in the carrier of (SCM R) \ {NAT} by XBOOLE_0:def 5;
then o in SCM-Data-Loc by SCMRING2:25;
hence o is Data-Location of R by AMI_2:def 16; :: thesis: verum