theorem :: AMI_3:20

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