let x be set ; :: thesis: for R being good Ring holds
( x is Data-Location of R iff x in SCM-Data-Loc )
let R be good Ring; :: thesis: ( x is Data-Location of R iff x in SCM-Data-Loc )
A1: the carrier of (SCM R) = ({(IC SCM )} \/ SCM-Data-Loc ) \/ NAT by Def1, AMI_5:23;
A2: the carrier of (SCM R) = SCM-Memory by Def1;

hereby :: thesis: ( x in SCM-Data-Loc implies x is Data-Location of R )

assume A3: x is Data-Location of R ; :: thesis: x in SCM-Data-Loc
then x in the carrier of (SCM R) \ (NAT \/ {NAT }) by Def2;
then ( x in the carrier of (SCM R) & not x in NAT \/ {NAT } ) by XBOOLE_0:def 5;
then A4: ( not x in NAT & not x in {NAT } ) by XBOOLE_0:def 3;
then x in {(IC SCM )} \/ SCM-Data-Loc by A1, A3, XBOOLE_0:def 3;
hence x in SCM-Data-Loc by A4, AMI_3:4, XBOOLE_0:def 3; :: thesis: verum

end;

assume A5: x in SCM-Data-Loc ; :: thesis: x is Data-Location of R
then x is Data-Location by AMI_3:def 2;
then x <> NAT by AMI_3:4, AMI_5:20;
then ( not x in NAT & not x in {NAT } ) by A5, AMI_2:29, TARSKI:def 1, XBOOLE_0:3;
then not x in NAT \/ {NAT } by XBOOLE_0:def 3;
then x in the carrier of (SCM R) \ (NAT \/ {NAT }) by A2, A5, XBOOLE_0:def 5;
hence x is Data-Location of R by Def2; :: thesis: verum