theorem :: AMI_3:17

for a, b being Data-Location holds not AddTo (a,b) is halting by Lm5;