let I be Int-Location; :: thesis: I is Data-Location
I in SCM-Data-Loc by AMI_2:def 16;
hence I is Data-Location ; :: thesis: verum