let dl be Int-Location ; :: thesis: dl <> IC
dl in SCM+FSA-Data-Loc by Def4;
then A1: dl in [:{1},NAT:] ;
not NAT in [:{1},NAT:] by FINSET_1:34;
hence dl <> IC by A1, Th7; :: thesis: verum