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