let I be Int-Location ; :: thesis: I is Data-Location
I in SCM-Data-Loc by Def4;
hence I is Data-Location by AMI_3:def 2; :: thesis: verum