let x be set ; :: thesis: for R being good Ring holds
( x is Data-Location of R iff x in Data-Locations )
let R be good Ring; :: thesis: ( x is Data-Location of R iff x in Data-Locations )
A1: IC = NAT by Def1;
A2: IC = NAT by AMI_3:1;
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 ) by XBOOLE_1:45;
thus ( x is Data-Location of R implies x in Data-Locations ) by Def2, A2, A3; :: thesis: ( x in Data-Locations implies x is Data-Location of R )
assume A9: x in Data-Locations ; :: thesis: x is Data-Location of R
then x is Data-Location by AMI_3:27, AMI_3:def 2;
then x <> NAT by AMI_3:1, AMI_5:2;
then A10: not x in {NAT} by TARSKI:def 1;
not x in {NAT} by A10;
then x in the carrier of (SCM R) \ {NAT} by A4, A9, XBOOLE_0:def 5;
hence x is Data-Location of R by Def2; :: thesis: verum