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