let l be Data-Location; :: thesis: Values l = INT
l in SCM-Data-Loc by AMI_2:def 16;
hence Values l = INT by AMI_2:7; :: thesis: verum