assume IC SCMPDS in SCM-Data-Loc ; :: thesis: contradiction
then IC SCMPDS is Int_position by SCMPDS_2:9;
then ObjectKind (IC SCMPDS ) = INT by SCMPDS_2:13;
hence contradiction by COMPOS_1:def 6, NUMBERS:27; :: thesis: verum