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