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) = SCM-Memory by Def1;
A2: the carrier of (SCM R) = ({(IC SCM )} \/ SCM-Data-Loc ) \/ NAT by Def1, AMI_5:23;

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 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 )} \/ SCM-Data-Loc by A2, A3, XBOOLE_0:def 3;
not x in {NAT } by A4, XBOOLE_0:def 3;
hence x in SCM-Data-Loc by A5, AMI_3:4, XBOOLE_0:def 3; :: thesis: verum

end;

assume A6: 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 A7: not x in {NAT } by TARSKI:def 1;
not x in NAT by A6, AMI_2:29, 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