let R be good Ring; :: thesis: for p being FinPartState of (SCM R) holds
( p is data-only iff dom p c= SCM-Data-Loc )
let p be FinPartState of (SCM R); :: thesis: ( p is data-only iff dom p c= SCM-Data-Loc )
Data-Locations (SCM R) = SCM-Data-Loc by SCMRING2:31;
hence ( p is data-only iff dom p c= SCM-Data-Loc ) by AMI_1:139; :: thesis: verum