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

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

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

end;

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