reconsider t = t as Element of SCM-Data-Loc by Def1;
A: t in SCM-Data-Loc ;
then t in Data-Locations by AMI_3:27;
then reconsider t = t as Object of SCM ;
t is Data-Location by A, AMI_3:def 2;
hence t is Data-Location ; :: thesis: verum