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

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