let il be Nat; :: thesis: for dl being FinSeq-Location holds il <> dl
let dl be FinSeq-Location ; :: thesis: il <> dl
A1: dl in INT \ NAT by Def3;
A2: il in NAT by ORDINAL1:def 12;
NAT misses INT \ NAT by XBOOLE_1:79;
hence il <> dl by A1, A2, XBOOLE_0:3; :: thesis: verum