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 & 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:27, SCMRING1:4; :: thesis: verum