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