theorem :: AMI_3:18

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