let R be good Ring; :: thesis: for a being Data-Location of R holds ObjectKind a = the carrier of R
let a be Data-Location of R; :: thesis: ObjectKind a = the carrier of R
( a in Data-Locations SCM & the Object-Kind of (SCM R) = SCM-OK R ) by SCMRING2:1, SCMRING2:def 1;
hence ObjectKind a = the carrier of R by AMI_3:72, SCMRING1:5; :: thesis: verum