let il be Element of NAT ; :: thesis: for dl being Int_position holds il <> dl
let dl be Int_position ; :: thesis: il <> dl
ObjectKind dl = INT by Th13;
hence il <> dl by COMPOS_1:def 8, SCMPDS_1:17; :: thesis: verum