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: IC = NAT by Def1;
A2: IC = NAT by AMI_3:4;
A3: the carrier of (SCM R) = SCM-Memory by Def1
.= the carrier of SCM ;
A4: the carrier of (SCM R) = SCM-Memory by Def1;
A5: the carrier of (SCM R) = ({(IC )} \/ (Data-Locations (SCM R))) \/ NAT by COMPOS_1:160;

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

assume A6: 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 A7: not x in NAT \/ {NAT} by XBOOLE_0:def 5;
then not x in NAT by XBOOLE_0:def 3;
then A8: x in {(IC )} \/ (Data-Locations (SCM R)) by A5, A6, XBOOLE_0:def 3;
not x in {NAT} by A7, XBOOLE_0:def 3;
then x in the carrier of (SCM R) \ (NAT \/ {NAT}) by A8, XBOOLE_0:def 3, A1, A2;
then x in the carrier of SCM \ ({(IC )} \/ NAT) by A2, A3;
hence x in Data-Locations SCM by A8, XBOOLE_0:def 3; :: thesis: verum

end;

assume A9: 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 A10: not x in {NAT} by TARSKI:def 1;
not x in NAT by A9, AMI_2:29, AMI_3:72, XBOOLE_0:3;
then not x in NAT \/ {NAT} by A10, XBOOLE_0:def 3;
then x in the carrier of (SCM R) \ (NAT \/ {NAT}) by A4, A9, XBOOLE_0:def 5;
hence x is Data-Location of R by Def2; :: thesis: verum