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