let l be Data-Location ; :: thesis: ObjectKind l = INT
l in SCM-Data-Loc by Def2;
hence ObjectKind l = INT by AMI_2:8; :: thesis: verum