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