theorem :: SCMRING4:4
for R being non trivial Ring
for s being State of (SCM R) holds Data-Locations c= dom s