let l be Int_position ; :: thesis: ObjectKind l = INT
l in SCM-Data-Loc by Def2;
hence ObjectKind l = INT by SCMPDS_1:21; :: thesis: verum