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