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_2:def 16, AMI_3:27;
hence b is Data-Location ; :: thesis: verum