let I be Int_position ; :: thesis: I is Data-Location
I in SCM-Data-Loc by Def2;
hence I is Data-Location by AMI_3:def 1, AMI_3:def 2; :: thesis: verum