let dl be Data-Location ; :: thesis: dl <> IC SCM
ex i being Element of NAT st dl = dl. i by Th18;
hence dl <> IC SCM by AMI_3:57; :: thesis: verum