for dl being Int-Location holds dl <> IC by AMI_2:def 16, Th1, FINSET_1:15;