[1,(abs (m + n))] in SCM-Data-Loc by AMI_2:24;
hence [1,(abs (m + n))] is Int_position by Def2; :: thesis: verum