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:13; :: thesis: verum