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