dl. k in SCM-Data-Loc by AMI_3:def 2;
hence dl. k is Int_position by SCMPDS_2:def 1, SCMPDS_2:def 2; :: thesis: verum