let dl be Int_position ; :: thesis: dl <> IC SCMPDS
ObjectKind dl = INT by Th13;
hence dl <> IC SCMPDS by COMPOS_1:def 6, NUMBERS:27; :: thesis: verum