theorem :: AMI_5:3

for il being Nat
for dl being Data-Location holds il <> dl