let il be Instruction-Location of SCMPDS ; :: thesis: for dl being Int_position holds il <> dl
let dl be Int_position ; :: thesis: il <> dl
( ObjectKind dl = INT & ObjectKind il = the Instructions of SCMPDS ) by Th13, AMI_1:def 14;
hence il <> dl by SCMPDS_1:17; :: thesis: verum