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