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