let il be Element of NAT ; :: thesis: for dl being FinSeq-Location holds il <> dl
let dl be FinSeq-Location ; :: thesis: il <> dl
A1: dl in INT \ NAT by Def5;
NAT misses INT \ NAT by XBOOLE_1:79;
hence il <> dl by A1, XBOOLE_0:3; :: thesis: verum