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
A1: a in SCM-Data-Loc by SCMRING2:1;
the Object-Kind of (SCM R) = SCM-OK R by SCMRING2:def 1;
hence ObjectKind a = the carrier of R by A1, SCMRING1:5; :: thesis: verum