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

( 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