reconsider t9 = t as Element of SCM-Data-Loc by Def1;
reconsider t9 = t9 as Object of SCM ;
t9 is Data-Location by AMI_3:def 2;
hence t is Data-Location ; :: thesis: verum