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