let R be Ring; :: thesis: Data-Locations = Data-Locations
Data-Locations misses {NAT} by AMI_2:20, AMI_3:27, ZFMISC_1:50;
then A1: Data-Locations misses {NAT} ;
thus Data-Locations = SCM-Memory \ {(IC )} by Def1
.= SCM-Memory \ {NAT} by Def1
.= ((Data-Locations ) \/ {NAT}) \ {NAT} by AMI_3:27
.= (Data-Locations ) \ {NAT} by XBOOLE_1:40
.= Data-Locations by A1, XBOOLE_1:83 ; :: thesis: verum