let il be Element of NAT ; :: thesis: for dl being Int-Location holds il <> dl
let dl be Int-Location ; :: thesis: il <> dl
dl in [:{1},NAT:] by Def4;
then ex x, y being set st
( x in {1} & y in NAT & dl = [x,y] ) by ZFMISC_1:84;
hence il <> dl ; :: thesis: verum