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

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