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