let R be good Ring; :: thesis: the carrier of (SCM R) = ({(IC (SCM R))} \/ (Data-Locations SCM)) \/ NAT
IC (SCM R) = IC SCM by AMI_3:4, SCMRING2:9;
hence the carrier of (SCM R) = ({(IC (SCM R))} \/ (Data-Locations SCM)) \/ NAT by AMI_5:23, SCMRING2:def 1; :: thesis: verum