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