theorem :: AMI_5:4

for s being State of SCM
for d being Data-Location holds d in dom s