let b be Element of Data-Locations ; :: thesis: b is Data-Location
b in Data-Locations ;
then reconsider b = b as Object of SCM ;
b is Data-Location by AMI_3:27, AMI_3:def 2;
hence b is Data-Location ; :: thesis: verum