theorem :: AMI_3:28

for d being Data-Location holds d in Data-Locations by Th27, AMI_2:def 16;