theorem :: SCMRING2:23

for x being set
for R being Ring holds
( x is Data-Location of R iff x in Data-Locations )