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