let dl be FinSeq-Location ; :: thesis: dl <> IC

now :: thesis: not NAT in INT \ NAT

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

per cases ( NAT in NAT or NAT in [:{0},NAT:] ) by A1, XBOOLE_0:def 3;

suppose NAT in NAT ; :: thesis: contradiction

hence contradiction ; :: thesis: verum

end;

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

hence contradiction by FINSET_1:15; :: thesis: verum

end;

end;

end;

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