let il be Element of NAT ; :: thesis: for dl being Data-Location holds il <> dl
let dl be Data-Location ; :: thesis: il <> dl
ex j being Element of NAT st dl = dl. j by Th18;
hence il <> dl by AMI_3:56; :: thesis: verum