let R be good Ring; :: thesis: for s being State of (SCM R) holds SCM-Data-Loc c= dom s
let s be State of (SCM R); :: thesis: SCM-Data-Loc c= dom s
Data-Locations (SCM R) = SCM-Data-Loc by SCMRING2:31;
hence SCM-Data-Loc c= dom s by SCMNORM:13; :: thesis: verum