let dl be Int-Location ; :: thesis: dl <> IC
dl in [:{1},NAT:] by Def4;
hence dl <> IC by Th7, FINSET_1:15; :: thesis: verum