theorem :: AMI_3:16

for a, b being Data-Location holds not a := b is halting by Lm4;