let dl be FinSeq-Location ; :: thesis:

assume NAT in INT \ NAT ; :: thesis:
then A1: NAT in NAT \/ [:{0},NAT:] by NUMBERS:def 4, XBOOLE_0:def 5;

per cases by A1, XBOOLE_0:def 3;

suppose NAT in NAT ; :: thesis:

hence contradiction ; :: thesis:

end;

suppose NAT in [:{0},NAT:] ; :: thesis:

hence contradiction by FINSET_1:15; :: thesis:

end;

end;

end;

hence dl <> IC by Def3, Th1; :: thesis: